; benchmark generated from python API
(set-info :status unknown)
(declare-fun teams_list_feasible () Bool)
(declare-fun your_teams_feasible () Bool)
(declare-fun team_name_feasible () Bool)
(declare-fun main_1_collom_feasible () Bool)
(declare-fun explore_more_feasible () Bool)
(declare-fun explore_repo_feasible () Bool)
(declare-fun contributions_feasible () Bool)
(declare-fun rustls_feasible () Bool)
(declare-fun falcosecurity_feasible () Bool)
(declare-fun explore_feasible () Bool)
(declare-fun last_changes_body_kid_8_feasible () Bool)
(declare-fun last_changes_body_feasible () Bool)
(declare-fun last_changes_body_kid_7_feasible () Bool)
(declare-fun last_changes_body_kid_6_feasible () Bool)
(declare-fun last_changes_body_kid_5_feasible () Bool)
(declare-fun last_changes_body_kid_4_feasible () Bool)
(declare-fun last_changes_body_kid_3_feasible () Bool)
(declare-fun last_changes_body_kid_2_feasible () Bool)
(declare-fun last_changes_body_kid_1_feasible () Bool)
(declare-fun last_changes_body_kid_0_feasible () Bool)
(declare-fun last_changes_feasible () Bool)
(declare-fun last_changes_title_feasible () Bool)
(declare-fun the_state_of_oct_kid_2_feasible () Bool)
(declare-fun the_state_of_oct_feasible () Bool)
(declare-fun the_state_of_oct_kid_1_feasible () Bool)
(declare-fun the_state_of_oct_kid_0_feasible () Bool)
(declare-fun right_homes_feasible () Bool)
(declare-fun rec_right_icon_feasible () Bool)
(declare-fun rec_feasible () Bool)
(declare-fun rec_left_icon_feasible () Bool)
(declare-fun rec_word_feasible () Bool)
(declare-fun stars_feasible () Bool)
(declare-fun boolect_feasible () Bool)
(declare-fun recomend_for_you_feasible () Bool)
(declare-fun cvc_smile_feasible () Bool)
(declare-fun cvc_page_feasible () Bool)
(declare-fun cvc_changes_feasible () Bool)
(declare-fun cvc_version_feasible () Bool)
(declare-fun cvc_icon_feasible () Bool)
(declare-fun z3_smile_feasible () Bool)
(declare-fun z3_page_feasible () Bool)
(declare-fun changes_feasible () Bool)
(declare-fun z3_version_feasible () Bool)
(declare-fun z3_icon_feasible () Bool)
(declare-fun learn_more_feasible () Bool)
(declare-fun home_updates_feasible () Bool)
(declare-fun home_update_words_feasible () Bool)
(declare-fun updates_to_your_homepage_feasible () Bool)
(declare-fun filter_feasible () Bool)
(declare-fun home_title_feasible () Bool)
(declare-fun send_feedback_feasible () Bool)
(declare-fun home_icon_feasible () Bool)
(declare-fun left_homes_feasible () Bool)
(declare-fun right_2_collom_feasible () Bool)
(declare-fun right_1_collom_feasible () Bool)
(declare-fun home_collom_holder_feasible () Bool)
(declare-fun home_collom_feasible () Bool)
(declare-fun links_feasible () Bool)
(declare-fun side_bar_feasible () Bool)
(declare-fun recent_act_feasible () Bool)
(declare-fun show_more_feasible () Bool)
(declare-fun repos_feasible () Bool)
(declare-fun find_repo_feasible () Bool)
(declare-fun top_repo_feasible () Bool)
(declare-fun user_name_feasible () Bool)
(declare-fun main_2_collom_feasible () Bool)
(declare-fun person_feasible () Bool)
(declare-fun mails_2_feasible () Bool)
(declare-fun mails_1_feasible () Bool)
(declare-fun mail_feasible () Bool)
(declare-fun pull_feasible () Bool)
(declare-fun point_feasible () Bool)
(declare-fun add_feasible () Bool)
(declare-fun mails_holder_feasible () Bool)
(declare-fun search_holder_feasible () Bool)
(declare-fun dashbord_feasible () Bool)
(declare-fun github_icon_feasible () Bool)
(declare-fun less_icon_feasible () Bool)
(declare-fun main_holder_feasible () Bool)
(declare-fun title_feasible () Bool)
(declare-fun back_ground_feasible () Bool)
(declare-fun teams_list_hight () Real)
(declare-fun teams_list_width () Real)
(declare-fun your_teams_x () Real)
(declare-fun teams_list_x () Real)
(declare-fun your_teams_width () Real)
(declare-fun team_name_hight () Real)
(declare-fun team_name_width () Real)
(declare-fun team_name_x () Real)
(declare-fun team_name_y () Real)
(declare-fun teams_list_y () Real)
(declare-fun your_teams_hight () Real)
(declare-fun your_teams_y () Real)
(declare-fun left_homes_width () Real)
(declare-fun main_1_collom_width () Real)
(declare-fun left_homes_x () Real)
(declare-fun main_1_collom_x () Real)
(declare-fun side_bar_x () Real)
(declare-fun side_bar_width () Real)
(declare-fun left_homes_y () Real)
(declare-fun side_bar_hight () Real)
(declare-fun side_bar_y () Real)
(declare-fun main_1_collom_hight () Real)
(declare-fun main_1_collom_y () Real)
(declare-fun left_homes_hight () Real)
(declare-fun right_1_collom_y () Real)
(declare-fun right_1_collom_width () Real)
(declare-fun right_1_collom_x () Real)
(declare-fun home_collom_width () Real)
(declare-fun right_1_collom_hight () Real)
(declare-fun explore_more_hight () Real)
(declare-fun explore_more_width () Real)
(declare-fun explore_repo_x () Real)
(declare-fun contributions_width () Real)
(declare-fun contributions_x () Real)
(declare-fun explore_repo_width () Real)
(declare-fun contributions_hight () Real)
(declare-fun rustls_width () Real)
(declare-fun rustls_x () Real)
(declare-fun rustls_hight () Real)
(declare-fun falcosecurity_width () Real)
(declare-fun falcosecurity_x () Real)
(declare-fun falcosecurity_hight () Real)
(declare-fun explore_hight () Real)
(declare-fun explore_width () Real)
(declare-fun explore_more_x () Real)
(declare-fun explore_x () Real)
(declare-fun contributions_y () Real)
(declare-fun explore_more_y () Real)
(declare-fun rustls_y () Real)
(declare-fun falcosecurity_y () Real)
(declare-fun explore_y () Real)
(declare-fun explore_repo_hight () Real)
(declare-fun explore_repo_y () Real)
(declare-fun last_changes_body_kid_8_hight () Real)
(declare-fun last_changes_body_kid_8_width () Real)
(declare-fun last_changes_body_kid_7_hight () Real)
(declare-fun last_changes_body_kid_7_width () Real)
(declare-fun last_changes_body_kid_6_hight () Real)
(declare-fun last_changes_body_kid_6_width () Real)
(declare-fun last_changes_body_kid_5_hight () Real)
(declare-fun last_changes_body_kid_5_width () Real)
(declare-fun last_changes_body_kid_4_hight () Real)
(declare-fun last_changes_body_kid_4_width () Real)
(declare-fun last_changes_body_kid_3_hight () Real)
(declare-fun last_changes_body_kid_3_width () Real)
(declare-fun last_changes_body_kid_2_hight () Real)
(declare-fun last_changes_body_kid_2_width () Real)
(declare-fun last_changes_body_kid_1_hight () Real)
(declare-fun last_changes_body_kid_1_width () Real)
(declare-fun last_changes_body_kid_0_hight () Real)
(declare-fun last_changes_body_kid_0_width () Real)
(declare-fun last_changes_body_kid_8_y () Real)
(declare-fun last_changes_body_kid_7_y () Real)
(declare-fun last_changes_body_kid_6_y () Real)
(declare-fun last_changes_body_kid_5_y () Real)
(declare-fun last_changes_body_kid_4_y () Real)
(declare-fun last_changes_body_kid_3_y () Real)
(declare-fun last_changes_body_kid_2_y () Real)
(declare-fun last_changes_body_kid_1_y () Real)
(declare-fun last_changes_body_kid_0_y () Real)
(declare-fun last_changes_body_kid_8_x () Real)
(declare-fun last_changes_body_x () Real)
(declare-fun last_changes_body_kid_7_x () Real)
(declare-fun last_changes_body_kid_6_x () Real)
(declare-fun last_changes_body_kid_5_x () Real)
(declare-fun last_changes_body_kid_4_x () Real)
(declare-fun last_changes_body_kid_3_x () Real)
(declare-fun last_changes_body_kid_2_x () Real)
(declare-fun last_changes_body_kid_1_x () Real)
(declare-fun last_changes_body_kid_0_x () Real)
(declare-fun last_changes_body_hight () Real)
(declare-fun last_changes_body_y () Real)
(declare-fun last_changes_body_width () Real)
(declare-fun last_changes_title_hight () Real)
(declare-fun last_changes_title_y () Real)
(declare-fun last_changes_hight () Real)
(declare-fun last_changes_y () Real)
(declare-fun last_changes_x () Real)
(declare-fun last_changes_width () Real)
(declare-fun last_changes_title_width () Real)
(declare-fun last_changes_title_x () Real)
(declare-fun the_state_of_oct_hight () Real)
(declare-fun the_state_of_oct_kid_0_hight () Real)
(declare-fun the_state_of_oct_kid_2_hight () Real)
(declare-fun the_state_of_oct_kid_1_hight () Real)
(declare-fun the_state_of_oct_y () Real)
(declare-fun the_state_of_oct_kid_2_y () Real)
(declare-fun the_state_of_oct_kid_0_y () Real)
(declare-fun the_state_of_oct_kid_2_width () Real)
(declare-fun the_state_of_oct_kid_2_x () Real)
(declare-fun the_state_of_oct_width () Real)
(declare-fun the_state_of_oct_x () Real)
(declare-fun the_state_of_oct_kid_1_width () Real)
(declare-fun the_state_of_oct_kid_1_x () Real)
(declare-fun the_state_of_oct_kid_0_width () Real)
(declare-fun the_state_of_oct_kid_0_x () Real)
(declare-fun the_state_of_oct_kid_1_y () Real)
(declare-fun right_homes_y () Real)
(declare-fun right_2_collom_y () Real)
(declare-fun right_2_collom_width () Real)
(declare-fun right_2_collom_x () Real)
(declare-fun right_homes_width () Real)
(declare-fun right_homes_x () Real)
(declare-fun right_homes_hight () Real)
(declare-fun rec_right_icon_y () Real)
(declare-fun rec_y () Real)
(declare-fun rec_right_icon_hight () Real)
(declare-fun rec_hight () Real)
(declare-fun rec_right_icon_width () Real)
(declare-fun rec_word_hight () Real)
(declare-fun rec_word_y () Real)
(declare-fun rec_left_icon_width () Real)
(declare-fun rec_left_icon_x () Real)
(declare-fun rec_right_icon_x () Real)
(declare-fun rec_left_icon_hight () Real)
(declare-fun rec_left_icon_y () Real)
(declare-fun rec_x () Real)
(declare-fun boolect_hight () Real)
(declare-fun boolect_y () Real)
(declare-fun rec_word_width () Real)
(declare-fun rec_word_x () Real)
(declare-fun rec_width () Real)
(declare-fun stars_width () Real)
(declare-fun stars_hight () Real)
(declare-fun stars_y () Real)
(declare-fun stars_x () Real)
(declare-fun recomend_for_you_hight () Real)
(declare-fun recomend_for_you_y () Real)
(declare-fun boolect_x () Real)
(declare-fun boolect_width () Real)
(declare-fun recomend_for_you_width () Real)
(declare-fun recomend_for_you_x () Real)
(declare-fun cvc_smile_hight () Real)
(declare-fun cvc_smile_width () Real)
(declare-fun cvc_smile_y () Real)
(declare-fun cvc_page_hight () Real)
(declare-fun cvc_page_y () Real)
(declare-fun cvc_page_width () Real)
(declare-fun cvc_changes_width () Real)
(declare-fun cvc_page_x () Real)
(declare-fun cvc_changes_x () Real)
(declare-fun cvc_changes_hight () Real)
(declare-fun cvc_version_hight () Real)
(declare-fun cvc_version_width () Real)
(declare-fun cvc_icon_hight () Real)
(declare-fun cvc_icon_width () Real)
(declare-fun cvc_smile_x () Real)
(declare-fun cvc_version_x () Real)
(declare-fun cvc_icon_x () Real)
(declare-fun cvc_changes_y () Real)
(declare-fun cvc_version_y () Real)
(declare-fun cvc_icon_y () Real)
(declare-fun z3_smile_hight () Real)
(declare-fun z3_smile_width () Real)
(declare-fun z3_page_hight () Real)
(declare-fun z3_smile_y () Real)
(declare-fun z3_page_y () Real)
(declare-fun changes_x () Real)
(declare-fun z3_page_width () Real)
(declare-fun z3_page_x () Real)
(declare-fun changes_width () Real)
(declare-fun changes_hight () Real)
(declare-fun z3_version_hight () Real)
(declare-fun z3_version_width () Real)
(declare-fun z3_icon_hight () Real)
(declare-fun z3_icon_width () Real)
(declare-fun z3_smile_x () Real)
(declare-fun z3_version_x () Real)
(declare-fun z3_icon_x () Real)
(declare-fun changes_y () Real)
(declare-fun z3_version_y () Real)
(declare-fun z3_icon_y () Real)
(declare-fun home_update_words_hight () Real)
(declare-fun home_update_words_width () Real)
(declare-fun home_update_words_x () Real)
(declare-fun home_updates_x () Real)
(declare-fun home_updates_width () Real)
(declare-fun home_updates_hight () Real)
(declare-fun home_updates_y () Real)
(declare-fun learn_more_hight () Real)
(declare-fun learn_more_y () Real)
(declare-fun learn_more_width () Real)
(declare-fun updates_to_your_homepage_y () Real)
(declare-fun updates_to_your_homepage_hight () Real)
(declare-fun updates_to_your_homepage_width () Real)
(declare-fun home_update_words_y () Real)
(declare-fun learn_more_x () Real)
(declare-fun updates_to_your_homepage_x () Real)
(declare-fun send_feedback_x () Real)
(declare-fun filter_x () Real)
(declare-fun send_feedback_width () Real)
(declare-fun home_title_x () Real)
(declare-fun home_icon_x () Real)
(declare-fun home_icon_width () Real)
(declare-fun filter_width () Real)
(declare-fun home_title_hight () Real)
(declare-fun filter_hight () Real)
(declare-fun home_title_y () Real)
(declare-fun filter_y () Real)
(declare-fun home_title_width () Real)
(declare-fun send_feedback_hight () Real)
(declare-fun send_feedback_y () Real)
(declare-fun home_icon_y () Real)
(declare-fun home_icon_hight () Real)
(declare-fun right_2_collom_hight () Real)
(declare-fun home_collom_y () Real)
(declare-fun home_collom_holder_y () Real)
(declare-fun home_collom_holder_width () Real)
(declare-fun home_collom_x () Real)
(declare-fun home_collom_holder_x () Real)
(declare-fun home_collom_holder_hight () Real)
(declare-fun home_collom_hight () Real)
(declare-fun links_x () Real)
(declare-fun links_width () Real)
(declare-fun links_hight () Real)
(declare-fun recent_act_width () Real)
(declare-fun recent_act_hight () Real)
(declare-fun show_more_width () Real)
(declare-fun show_more_hight () Real)
(declare-fun repos_width () Real)
(declare-fun repos_x () Real)
(declare-fun repos_hight () Real)
(declare-fun find_repo_width () Real)
(declare-fun find_repo_x () Real)
(declare-fun find_repo_hight () Real)
(declare-fun top_repo_width () Real)
(declare-fun top_repo_x () Real)
(declare-fun top_repo_hight () Real)
(declare-fun user_name_width () Real)
(declare-fun user_name_hight () Real)
(declare-fun recent_act_x () Real)
(declare-fun show_more_x () Real)
(declare-fun user_name_x () Real)
(declare-fun links_y () Real)
(declare-fun recent_act_y () Real)
(declare-fun show_more_y () Real)
(declare-fun repos_y () Real)
(declare-fun find_repo_y () Real)
(declare-fun top_repo_y () Real)
(declare-fun user_name_y () Real)
(declare-fun main_2_collom_y () Real)
(declare-fun main_2_collom_hight () Real)
(declare-fun main_2_collom_width () Real)
(declare-fun main_2_collom_x () Real)
(declare-fun main_holder_hight () Real)
(declare-fun main_holder_y () Real)
(declare-fun main_holder_width () Real)
(declare-fun main_holder_x () Real)
(declare-fun mail_width () Real)
(declare-fun mail_x () Real)
(declare-fun person_x () Real)
(declare-fun person_y () Real)
(declare-fun mails_2_hight () Real)
(declare-fun mails_2_y () Real)
(declare-fun person_hight () Real)
(declare-fun person_width () Real)
(declare-fun mails_2_width () Real)
(declare-fun mails_2_x () Real)
(declare-fun mail_hight () Real)
(declare-fun mail_y () Real)
(declare-fun pull_width () Real)
(declare-fun point_width () Real)
(declare-fun add_width () Real)
(declare-fun pull_x () Real)
(declare-fun point_x () Real)
(declare-fun add_x () Real)
(declare-fun mails_1_y () Real)
(declare-fun mails_1_hight () Real)
(declare-fun pull_hight () Real)
(declare-fun pull_y () Real)
(declare-fun point_hight () Real)
(declare-fun point_y () Real)
(declare-fun add_hight () Real)
(declare-fun add_y () Real)
(declare-fun mails_1_width () Real)
(declare-fun mails_1_x () Real)
(declare-fun search_holder_x () Real)
(declare-fun mails_holder_x () Real)
(declare-fun search_holder_width () Real)
(declare-fun mails_holder_hight () Real)
(declare-fun mails_holder_y () Real)
(declare-fun mails_holder_width () Real)
(declare-fun dashbord_x () Real)
(declare-fun dashbord_width () Real)
(declare-fun search_bar_2_width () Real)
(declare-fun search_bar_1_width () Real)
(declare-fun search_bar_2_feasible () Bool)
(declare-fun search_bar_1_feasible () Bool)
(declare-fun search_bar_2_y () Real)
(declare-fun search_holder_hight () Real)
(declare-fun search_holder_y () Real)
(declare-fun search_bar_2_hight () Real)
(declare-fun search_bar_2_x () Real)
(declare-fun search_bar_1_hight () Real)
(declare-fun search_bar_1_y () Real)
(declare-fun search_bar_1_x () Real)
(declare-fun github_icon_width () Real)
(declare-fun github_icon_x () Real)
(declare-fun less_icon_width () Real)
(declare-fun less_icon_x () Real)
(declare-fun title_hight () Real)
(declare-fun title_y () Real)
(declare-fun dashbord_hight () Real)
(declare-fun dashbord_y () Real)
(declare-fun github_icon_y () Real)
(declare-fun github_icon_hight () Real)
(declare-fun less_icon_hight () Real)
(declare-fun less_icon_y () Real)
(declare-fun title_width () Real)
(declare-fun title_x () Real)
(declare-fun BC_y () Real)
(declare-fun back_ground_y () Real)
(declare-fun back_ground_x () Real)
(declare-fun BC_width () Real)
(declare-fun back_ground_width () Real)
(declare-fun BC_x () Real)
(declare-fun back_ground_hight () Real)
(declare-fun BC_feasible () Bool)
(declare-fun BC_hight () Real)
(assert
 (let (($x3118 (not your_teams_feasible)))
 (let (($x3374 (or $x3118 teams_list_feasible)))
 (let (($x3372 (not teams_list_feasible)))
 (let (($x3373 (or $x3372 your_teams_feasible)))
 (let (($x3371 (or $x3118 team_name_feasible)))
 (let (($x3369 (not team_name_feasible)))
 (let (($x3370 (or $x3369 your_teams_feasible)))
 (let (($x1004 (not main_1_collom_feasible)))
 (let (($x3368 (or $x1004 your_teams_feasible)))
 (let (($x3367 (or $x3118 main_1_collom_feasible)))
 (let (($x2839 (not explore_repo_feasible)))
 (let (($x3366 (or $x2839 explore_more_feasible)))
 (let (($x3364 (not explore_more_feasible)))
 (let (($x3365 (or $x3364 explore_repo_feasible)))
 (let (($x3363 (or $x2839 contributions_feasible)))
 (let (($x3361 (not contributions_feasible)))
 (let (($x3362 (or $x3361 explore_repo_feasible)))
 (let (($x3360 (or $x2839 rustls_feasible)))
 (let (($x3358 (not rustls_feasible)))
 (let (($x3359 (or $x3358 explore_repo_feasible)))
 (let (($x3357 (or $x2839 falcosecurity_feasible)))
 (let (($x3355 (not falcosecurity_feasible)))
 (let (($x3356 (or $x3355 explore_repo_feasible)))
 (let (($x3354 (or $x2839 explore_feasible)))
 (let (($x3352 (not explore_feasible)))
 (let (($x3353 (or $x3352 explore_repo_feasible)))
 (let (($x2572 (not last_changes_body_feasible)))
 (let (($x3351 (or $x2572 last_changes_body_kid_8_feasible)))
 (let (($x3349 (not last_changes_body_kid_8_feasible)))
 (let (($x3350 (or $x3349 last_changes_body_feasible)))
 (let (($x3348 (or $x2572 last_changes_body_kid_7_feasible)))
 (let (($x3346 (not last_changes_body_kid_7_feasible)))
 (let (($x3347 (or $x3346 last_changes_body_feasible)))
 (let (($x3345 (or $x2572 last_changes_body_kid_6_feasible)))
 (let (($x3343 (not last_changes_body_kid_6_feasible)))
 (let (($x3344 (or $x3343 last_changes_body_feasible)))
 (let (($x3342 (or $x2572 last_changes_body_kid_5_feasible)))
 (let (($x3340 (not last_changes_body_kid_5_feasible)))
 (let (($x3341 (or $x3340 last_changes_body_feasible)))
 (let (($x3339 (or $x2572 last_changes_body_kid_4_feasible)))
 (let (($x3337 (not last_changes_body_kid_4_feasible)))
 (let (($x3338 (or $x3337 last_changes_body_feasible)))
 (let (($x3336 (or $x2572 last_changes_body_kid_3_feasible)))
 (let (($x3334 (not last_changes_body_kid_3_feasible)))
 (let (($x3335 (or $x3334 last_changes_body_feasible)))
 (let (($x3333 (or $x2572 last_changes_body_kid_2_feasible)))
 (let (($x3331 (not last_changes_body_kid_2_feasible)))
 (let (($x3332 (or $x3331 last_changes_body_feasible)))
 (let (($x3330 (or $x2572 last_changes_body_kid_1_feasible)))
 (let (($x3328 (not last_changes_body_kid_1_feasible)))
 (let (($x3329 (or $x3328 last_changes_body_feasible)))
 (let (($x3327 (or $x2572 last_changes_body_kid_0_feasible)))
 (let (($x3325 (not last_changes_body_kid_0_feasible)))
 (let (($x3326 (or $x3325 last_changes_body_feasible)))
 (let (($x2470 (not last_changes_feasible)))
 (let (($x3324 (or $x2470 last_changes_body_feasible)))
 (let (($x3323 (or $x2572 last_changes_feasible)))
 (let (($x3322 (or $x2470 last_changes_title_feasible)))
 (let (($x3320 (not last_changes_title_feasible)))
 (let (($x3321 (or $x3320 last_changes_feasible)))
 (let (($x2364 (not the_state_of_oct_feasible)))
 (let (($x3319 (or $x2364 the_state_of_oct_kid_2_feasible)))
 (let (($x3317 (not the_state_of_oct_kid_2_feasible)))
 (let (($x3318 (or $x3317 the_state_of_oct_feasible)))
 (let (($x3316 (or $x2364 the_state_of_oct_kid_1_feasible)))
 (let (($x3314 (not the_state_of_oct_kid_1_feasible)))
 (let (($x3315 (or $x3314 the_state_of_oct_feasible)))
 (let (($x3313 (or $x2364 the_state_of_oct_kid_0_feasible)))
 (let (($x3311 (not the_state_of_oct_kid_0_feasible)))
 (let (($x3312 (or $x3311 the_state_of_oct_feasible)))
 (let (($x2256 (not right_homes_feasible)))
 (let (($x3310 (or $x2256 explore_repo_feasible)))
 (let (($x3309 (or $x2839 right_homes_feasible)))
 (let (($x3308 (or $x2256 last_changes_feasible)))
 (let (($x3307 (or $x2470 right_homes_feasible)))
 (let (($x3306 (or $x2256 the_state_of_oct_feasible)))
 (let (($x3305 (or $x2364 right_homes_feasible)))
 (let (($x2144 (not rec_feasible)))
 (let (($x3304 (or $x2144 rec_right_icon_feasible)))
 (let (($x3302 (not rec_right_icon_feasible)))
 (let (($x3303 (or $x3302 rec_feasible)))
 (let (($x3301 (or $x2144 rec_left_icon_feasible)))
 (let (($x3299 (not rec_left_icon_feasible)))
 (let (($x3300 (or $x3299 rec_feasible)))
 (let (($x3298 (or $x2144 rec_word_feasible)))
 (let (($x3296 (not rec_word_feasible)))
 (let (($x3297 (or $x3296 rec_feasible)))
 (let (($x3295 (or $x2144 stars_feasible)))
 (let (($x3293 (not stars_feasible)))
 (let (($x3294 (or $x3293 rec_feasible)))
 (let (($x3292 (or $x2144 boolect_feasible)))
 (let (($x3290 (not boolect_feasible)))
 (let (($x3291 (or $x3290 rec_feasible)))
 (let (($x3289 (or $x2144 recomend_for_you_feasible)))
 (let (($x3287 (not recomend_for_you_feasible)))
 (let (($x3288 (or $x3287 rec_feasible)))
 (let (($x2020 (not cvc_page_feasible)))
 (let (($x3286 (or $x2020 cvc_smile_feasible)))
 (let (($x3284 (not cvc_smile_feasible)))
 (let (($x3285 (or $x3284 cvc_page_feasible)))
 (let (($x3283 (or $x2020 cvc_changes_feasible)))
 (let (($x3281 (not cvc_changes_feasible)))
 (let (($x3282 (or $x3281 cvc_page_feasible)))
 (let (($x3280 (or $x2020 cvc_version_feasible)))
 (let (($x3278 (not cvc_version_feasible)))
 (let (($x3279 (or $x3278 cvc_page_feasible)))
 (let (($x3277 (or $x2020 cvc_icon_feasible)))
 (let (($x3275 (not cvc_icon_feasible)))
 (let (($x3276 (or $x3275 cvc_page_feasible)))
 (let (($x1882 (not z3_page_feasible)))
 (let (($x3274 (or $x1882 z3_smile_feasible)))
 (let (($x3272 (not z3_smile_feasible)))
 (let (($x3273 (or $x3272 z3_page_feasible)))
 (let (($x3271 (or $x1882 changes_feasible)))
 (let (($x3269 (not changes_feasible)))
 (let (($x3270 (or $x3269 z3_page_feasible)))
 (let (($x3268 (or $x1882 z3_version_feasible)))
 (let (($x3266 (not z3_version_feasible)))
 (let (($x3267 (or $x3266 z3_page_feasible)))
 (let (($x3265 (or $x1882 z3_icon_feasible)))
 (let (($x3263 (not z3_icon_feasible)))
 (let (($x3264 (or $x3263 z3_page_feasible)))
 (let (($x1773 (not home_updates_feasible)))
 (let (($x3262 (or $x1773 learn_more_feasible)))
 (let (($x3260 (not learn_more_feasible)))
 (let (($x3261 (or $x3260 home_updates_feasible)))
 (let (($x3259 (or $x1773 home_update_words_feasible)))
 (let (($x3257 (not home_update_words_feasible)))
 (let (($x3258 (or $x3257 home_updates_feasible)))
 (let (($x3256 (or $x1773 updates_to_your_homepage_feasible)))
 (let (($x3254 (not updates_to_your_homepage_feasible)))
 (let (($x3255 (or $x3254 home_updates_feasible)))
 (let (($x1660 (not home_title_feasible)))
 (let (($x3253 (or $x1660 filter_feasible)))
 (let (($x3251 (not filter_feasible)))
 (let (($x3252 (or $x3251 home_title_feasible)))
 (let (($x3250 (or $x1660 send_feedback_feasible)))
 (let (($x3248 (not send_feedback_feasible)))
 (let (($x3249 (or $x3248 home_title_feasible)))
 (let (($x3247 (or $x1660 home_icon_feasible)))
 (let (($x3245 (not home_icon_feasible)))
 (let (($x3246 (or $x3245 home_title_feasible)))
 (let (($x1491 (not left_homes_feasible)))
 (let (($x3244 (or $x1491 rec_feasible)))
 (let (($x3243 (or $x2144 left_homes_feasible)))
 (let (($x3242 (or $x1491 cvc_page_feasible)))
 (let (($x3241 (or $x2020 left_homes_feasible)))
 (let (($x3240 (or $x1491 z3_page_feasible)))
 (let (($x3239 (or $x1882 left_homes_feasible)))
 (let (($x3238 (or $x1491 home_updates_feasible)))
 (let (($x3237 (or $x1773 left_homes_feasible)))
 (let (($x3236 (or $x1491 home_title_feasible)))
 (let (($x3235 (or $x1660 left_homes_feasible)))
 (let (($x1370 (not right_2_collom_feasible)))
 (let (($x3234 (or $x1370 right_homes_feasible)))
 (let (($x3233 (or $x2256 right_2_collom_feasible)))
 (let (($x1385 (not right_1_collom_feasible)))
 (let (($x3232 (or $x1385 $x1004 $x1491)))
 (let (($x3231 (or $x1370 $x1004 $x1491)))
 (let (($x3230 (or $x1370 $x1385 $x1491)))
 (let (($x3229 (or right_2_collom_feasible right_1_collom_feasible main_1_collom_feasible $x1491)))
 (let (($x3228 (or $x1004 left_homes_feasible)))
 (let (($x3227 (or $x1385 left_homes_feasible)))
 (let (($x3226 (or $x1370 left_homes_feasible)))
 (let (($x3225 (or $x1385 home_collom_holder_feasible)))
 (let (($x3224 (or $x1370 home_collom_holder_feasible)))
 (let (($x1344 (not home_collom_feasible)))
 (let (($x3223 (or $x1344 home_collom_holder_feasible)))
 (let (($x1402 (not home_collom_holder_feasible)))
 (let (($x3222 (or $x1402 home_collom_feasible)))
 (let (($x1122 (not side_bar_feasible)))
 (let (($x3221 (or $x1122 links_feasible)))
 (let (($x3219 (not links_feasible)))
 (let (($x3220 (or $x3219 side_bar_feasible)))
 (let (($x3218 (or $x1122 recent_act_feasible)))
 (let (($x3216 (not recent_act_feasible)))
 (let (($x3217 (or $x3216 side_bar_feasible)))
 (let (($x3215 (or $x1122 show_more_feasible)))
 (let (($x3213 (not show_more_feasible)))
 (let (($x3214 (or $x3213 side_bar_feasible)))
 (let (($x3212 (or $x1122 repos_feasible)))
 (let (($x3210 (not repos_feasible)))
 (let (($x3211 (or $x3210 side_bar_feasible)))
 (let (($x3209 (or $x1122 find_repo_feasible)))
 (let (($x3207 (not find_repo_feasible)))
 (let (($x3208 (or $x3207 side_bar_feasible)))
 (let (($x3206 (or $x1122 top_repo_feasible)))
 (let (($x3204 (not top_repo_feasible)))
 (let (($x3205 (or $x3204 side_bar_feasible)))
 (let (($x3203 (or $x1122 user_name_feasible)))
 (let (($x3201 (not user_name_feasible)))
 (let (($x3202 (or $x3201 side_bar_feasible)))
 (let (($x988 (not main_2_collom_feasible)))
 (let (($x3200 (or $x988 home_collom_feasible)))
 (let (($x3199 (or $x1344 main_2_collom_feasible)))
 (let (($x3198 (or $x988 $x1004 $x1122)))
 (let (($x3197 (or main_2_collom_feasible main_1_collom_feasible $x1122)))
 (let (($x3196 (or $x1004 side_bar_feasible)))
 (let (($x3195 (or $x988 side_bar_feasible)))
 (let (($x3192 (not person_feasible)))
 (let (($x722 (not mails_2_feasible)))
 (let (($x704 (not mails_1_feasible)))
 (let (($x3194 (or $x704 $x722 $x3192)))
 (let (($x3193 (or mails_1_feasible mails_2_feasible $x3192)))
 (let (($x3191 (or $x722 person_feasible)))
 (let (($x3190 (or $x704 person_feasible)))
 (let (($x3187 (not mail_feasible)))
 (let (($x3189 (or $x704 $x722 $x3187)))
 (let (($x3188 (or mails_1_feasible mails_2_feasible $x3187)))
 (let (($x3186 (or $x722 mail_feasible)))
 (let (($x3185 (or $x704 mail_feasible)))
 (let (($x3184 (or $x704 pull_feasible)))
 (let (($x3182 (not pull_feasible)))
 (let (($x3183 (or $x3182 mails_1_feasible)))
 (let (($x3181 (or $x704 point_feasible)))
 (let (($x3179 (not point_feasible)))
 (let (($x3180 (or $x3179 mails_1_feasible)))
 (let (($x3178 (or $x704 add_feasible)))
 (let (($x3176 (not add_feasible)))
 (let (($x3177 (or $x3176 mails_1_feasible)))
 (let (($x3175 (or $x3118 (= teams_list_hight 100.0))))
 (let ((?x3171 (+ (- (+ (- your_teams_width) teams_list_x) your_teams_x) teams_list_width)))
 (let (($x3173 (or $x3118 (= ?x3171 (- 20.0)))))
 (let (($x3167 (= (+ (- 50.0) team_name_hight) 0.0)))
 (let (($x3165 (= (+ (- 100.0) team_name_width) 0.0)))
 (let (($x3163 (or $x3118 (= (- teams_list_x your_teams_x) 20.0))))
 (let (($x3161 (or $x3118 (= (+ (- your_teams_x) team_name_x) 20.0))))
 (let (($x3159 (or $x3118 (>= (- (- teams_list_y team_name_y) team_name_hight) 0.0))))
 (let ((?x3155 (+ (- (+ (- teams_list_y) your_teams_y) teams_list_hight) your_teams_hight)))
 (let (($x3157 (or $x3118 (>= ?x3155 20.0))))
 (let (($x3151 (or $x3118 (>= (- teams_list_y your_teams_y) 20.0))))
 (let ((?x3146 (- (+ (- your_teams_width teams_list_x) your_teams_x) teams_list_width)))
 (let (($x3148 (or $x3118 (>= ?x3146 20.0))))
 (let (($x3143 (or $x3118 (>= (- teams_list_x your_teams_x) 20.0))))
 (let ((?x3138 (+ (- (- your_teams_y team_name_y) team_name_hight) your_teams_hight)))
 (let (($x3140 (or $x3118 (>= ?x3138 20.0))))
 (let (($x3135 (or $x3118 (>= (+ (- your_teams_y) team_name_y) 20.0))))
 (let ((?x3130 (- (+ (+ (- team_name_width) your_teams_width) your_teams_x) team_name_x)))
 (let (($x3132 (or $x3118 (>= ?x3130 20.0))))
 (let (($x3126 (or $x3118 (>= (+ (- your_teams_x) team_name_x) 20.0))))
 (let (($x3122 (or $x3118 (= (- (- teams_list_y team_name_y) team_name_hight) 20.0))))
 (let (($x3117 (>= teams_list_hight 0.0)))
 (let (($x3116 (>= teams_list_width 0.0)))
 (let (($x3115 (>= teams_list_y 0.0)))
 (let (($x3114 (>= teams_list_x 0.0)))
 (let (($x3113 (>= team_name_hight 0.0)))
 (let (($x3112 (>= team_name_width 0.0)))
 (let (($x3111 (>= team_name_y 0.0)))
 (let (($x3110 (>= team_name_x 0.0)))
 (let ((?x3107 (+ (- (+ (- main_1_collom_x) left_homes_x) main_1_collom_width) left_homes_width)))
 (let (($x3109 (or $x1004 (= ?x3107 (- 20.0)))))
 (let (($x3105 (or $x1004 (= (+ (- main_1_collom_x) left_homes_x) 20.0))))
 (let ((?x3101 (+ (- (+ (- main_1_collom_x) your_teams_width) main_1_collom_width) your_teams_x)))
 (let (($x3103 (or $x1004 (= ?x3101 (- 20.0)))))
 (let (($x3098 (or $x1004 (= (+ (- main_1_collom_x) your_teams_x) 20.0))))
 (let ((?x3094 (+ (- (+ (- main_1_collom_x) side_bar_width) main_1_collom_width) side_bar_x)))
 (let (($x3096 (or $x1004 (= ?x3094 (- 20.0)))))
 (let (($x3091 (or $x1004 (= (+ (- main_1_collom_x) side_bar_x) 20.0))))
 (let (($x3089 (or $x1004 (= (+ (- (- your_teams_y) your_teams_hight) left_homes_y) 20.0))))
 (let (($x3087 (or $x1004 (= (- (- your_teams_y side_bar_y) side_bar_hight) 20.0))))
 (let (($x3085 (or $x1004 (>= (+ (- (- your_teams_y) your_teams_hight) left_homes_y) 0.0))))
 (let (($x3081 (or $x1004 (>= (- (- your_teams_y side_bar_y) side_bar_hight) 0.0))))
 (let ((?x3075 (+ (- (+ (- left_homes_hight) main_1_collom_y) left_homes_y) main_1_collom_hight)))
 (let (($x3077 (or $x1004 (>= ?x3075 20.0))))
 (let (($x3072 (or $x1004 (>= (+ (- main_1_collom_y) left_homes_y) 20.0))))
 (let ((?x3066 (- (+ (- main_1_collom_x left_homes_x) main_1_collom_width) left_homes_width)))
 (let (($x3068 (or $x1004 (>= ?x3066 20.0))))
 (let (($x3063 (or $x1004 (>= (+ (- main_1_collom_x) left_homes_x) 20.0))))
 (let ((?x3058 (+ (- (+ (- your_teams_y) main_1_collom_y) your_teams_hight) main_1_collom_hight)))
 (let (($x3060 (or $x1004 (>= ?x3058 20.0))))
 (let (($x3054 (or $x1004 (>= (- your_teams_y main_1_collom_y) 20.0))))
 (let ((?x3049 (- (+ (- main_1_collom_x your_teams_width) main_1_collom_width) your_teams_x)))
 (let (($x3051 (or $x1004 (>= ?x3049 20.0))))
 (let (($x3046 (or $x1004 (>= (+ (- main_1_collom_x) your_teams_x) 20.0))))
 (let ((?x3041 (+ (- (+ (- side_bar_y) main_1_collom_y) side_bar_hight) main_1_collom_hight)))
 (let (($x3043 (or $x1004 (>= ?x3041 20.0))))
 (let (($x3038 (or $x1004 (>= (- side_bar_y main_1_collom_y) 20.0))))
 (let ((?x3033 (- (+ (- main_1_collom_x side_bar_width) main_1_collom_width) side_bar_x)))
 (let (($x3035 (or $x1004 (>= ?x3033 20.0))))
 (let (($x3030 (or $x1004 (>= (+ (- main_1_collom_x) side_bar_x) 20.0))))
 (let (($x3026 (>= your_teams_hight 0.0)))
 (let (($x3025 (>= your_teams_width 0.0)))
 (let (($x3024 (>= your_teams_y 0.0)))
 (let (($x3023 (>= your_teams_x 0.0)))
 (let (($x3022 (or $x1385 (= (+ (- right_1_collom_y) left_homes_y) 0.0))))
 (let ((?x3018 (+ (- (+ (- right_1_collom_x) left_homes_x) right_1_collom_width) left_homes_width)))
 (let (($x3020 (or $x1385 (= ?x3018 0.0))))
 (let (($x3016 (or $x1385 (= (+ (- right_1_collom_x) left_homes_x) 0.0))))
 (let (($x3008 (> home_collom_width 700.0)))
 (let (($x3014 (or $x3008 (= (- home_collom_width right_1_collom_width) 20.0))))
 (let (($x3010 (= right_1_collom_width 700.0)))
 (let (($x3011 (or (not $x3008) $x3010)))
 (let ((?x3004 (- (+ (+ (- left_homes_hight) right_1_collom_hight) right_1_collom_y) left_homes_y)))
 (let (($x3006 (or $x1385 (>= ?x3004 0.0))))
 (let (($x3000 (or $x1385 (>= (+ (- right_1_collom_y) left_homes_y) 0.0))))
 (let ((?x2994 (- (+ (- right_1_collom_x left_homes_x) right_1_collom_width) left_homes_width)))
 (let (($x2996 (or $x1385 (>= ?x2994 0.0))))
 (let (($x2991 (or $x1385 (>= (+ (- right_1_collom_x) left_homes_x) 0.0))))
 (let (($x2987 (= (+ (- 50.0) explore_more_hight) 0.0)))
 (let (($x2985 (= (+ (- 100.0) explore_more_width) 0.0)))
 (let ((?x2981 (- (+ (+ (- explore_repo_width) contributions_x) contributions_width) explore_repo_x)))
 (let (($x2983 (or $x2839 (= ?x2981 (- 20.0)))))
 (let (($x2978 (= (+ (- 100.0) contributions_hight) 0.0)))
 (let ((?x2974 (- (+ (+ (- explore_repo_width) rustls_x) rustls_width) explore_repo_x)))
 (let (($x2976 (or $x2839 (= ?x2974 (- 20.0)))))
 (let (($x2971 (= (+ (- 100.0) rustls_hight) 0.0)))
 (let ((?x2967 (- (+ (+ (- explore_repo_width) falcosecurity_x) falcosecurity_width) explore_repo_x)))
 (let (($x2969 (or $x2839 (= ?x2967 (- 20.0)))))
 (let (($x2963 (= (+ (- 100.0) falcosecurity_hight) 0.0)))
 (let (($x2961 (= (+ (- 50.0) explore_hight) 0.0)))
 (let (($x2959 (= (+ (- 100.0) explore_width) 0.0)))
 (let (($x2957 (or $x2839 (= (+ (- explore_repo_x) explore_more_x) 20.0))))
 (let (($x2955 (or $x2839 (= (- contributions_x explore_repo_x) 20.0))))
 (let (($x2953 (or $x2839 (= (- rustls_x explore_repo_x) 20.0))))
 (let (($x2951 (or $x2839 (= (- falcosecurity_x explore_repo_x) 20.0))))
 (let (($x2949 (or $x2839 (= (- explore_x explore_repo_x) 20.0))))
 (let ((?x2856 (- (+ (- contributions_hight) explore_more_y) contributions_y)))
 (let (($x2947 (or $x2839 (>= ?x2856 0.0))))
 (let (($x2945 (or $x2839 (>= (+ (- (- rustls_y) rustls_hight) contributions_y) 0.0))))
 (let ((?x2846 (- (+ (- falcosecurity_y) rustls_y) falcosecurity_hight)))
 (let (($x2943 (or $x2839 (>= ?x2846 0.0))))
 (let (($x2941 (or $x2839 (>= (- (- falcosecurity_y explore_y) explore_hight) 0.0))))
 (let ((?x2937 (- (+ (- explore_repo_y explore_more_y) explore_repo_hight) explore_more_hight)))
 (let (($x2939 (or $x2839 (>= ?x2937 20.0))))
 (let (($x2934 (or $x2839 (>= (+ (- explore_repo_y) explore_more_y) 20.0))))
 (let ((?x2929 (- (+ (- explore_repo_width explore_more_width) explore_repo_x) explore_more_x)))
 (let (($x2931 (or $x2839 (>= ?x2929 20.0))))
 (let (($x2926 (or $x2839 (>= (+ (- explore_repo_x) explore_more_x) 20.0))))
 (let ((?x2920 (- (+ (+ (- contributions_hight) explore_repo_y) explore_repo_hight) contributions_y)))
 (let (($x2922 (or $x2839 (>= ?x2920 20.0))))
 (let (($x2917 (or $x2839 (>= (+ (- explore_repo_y) contributions_y) 20.0))))
 (let ((?x2912 (+ (- (- explore_repo_width contributions_x) contributions_width) explore_repo_x)))
 (let (($x2914 (or $x2839 (>= ?x2912 20.0))))
 (let (($x2909 (or $x2839 (>= (- contributions_x explore_repo_x) 20.0))))
 (let ((?x2904 (+ (+ (- (- rustls_y) rustls_hight) explore_repo_y) explore_repo_hight)))
 (let (($x2906 (or $x2839 (>= ?x2904 20.0))))
 (let (($x2902 (or $x2839 (>= (- rustls_y explore_repo_y) 20.0))))
 (let ((?x2897 (+ (- (- explore_repo_width rustls_x) rustls_width) explore_repo_x)))
 (let (($x2899 (or $x2839 (>= ?x2897 20.0))))
 (let (($x2894 (or $x2839 (>= (- rustls_x explore_repo_x) 20.0))))
 (let ((?x2889 (+ (+ (- (- falcosecurity_y) falcosecurity_hight) explore_repo_y) explore_repo_hight)))
 (let (($x2891 (or $x2839 (>= ?x2889 20.0))))
 (let (($x2886 (or $x2839 (>= (- falcosecurity_y explore_repo_y) 20.0))))
 (let ((?x2881 (+ (- (- explore_repo_width falcosecurity_x) falcosecurity_width) explore_repo_x)))
 (let (($x2883 (or $x2839 (>= ?x2881 20.0))))
 (let (($x2878 (or $x2839 (>= (- falcosecurity_x explore_repo_x) 20.0))))
 (let ((?x2873 (+ (+ (- (- explore_y) explore_hight) explore_repo_y) explore_repo_hight)))
 (let (($x2875 (or $x2839 (>= ?x2873 20.0))))
 (let (($x2869 (or $x2839 (>= (- explore_y explore_repo_y) 20.0))))
 (let ((?x2864 (+ (- (- explore_repo_width explore_x) explore_width) explore_repo_x)))
 (let (($x2866 (or $x2839 (>= ?x2864 20.0))))
 (let (($x2861 (or $x2839 (>= (- explore_x explore_repo_x) 20.0))))
 (let (($x2858 (or $x2839 (= ?x2856 10.0))))
 (let (($x2853 (or $x2839 (= (+ (- (- rustls_y) rustls_hight) contributions_y) 10.0))))
 (let (($x2848 (or $x2839 (= ?x2846 10.0))))
 (let (($x2843 (or $x2839 (= (- (- falcosecurity_y explore_y) explore_hight) 10.0))))
 (let (($x2838 (>= explore_more_hight 0.0)))
 (let (($x2837 (>= explore_more_width 0.0)))
 (let (($x2836 (>= explore_more_y 0.0)))
 (let (($x2835 (>= explore_more_x 0.0)))
 (let (($x2834 (>= contributions_hight 0.0)))
 (let (($x2833 (>= contributions_width 0.0)))
 (let (($x2832 (>= contributions_y 0.0)))
 (let (($x2831 (>= contributions_x 0.0)))
 (let (($x2830 (>= rustls_hight 0.0)))
 (let (($x2829 (>= rustls_width 0.0)))
 (let (($x2828 (>= rustls_y 0.0)))
 (let (($x2827 (>= rustls_x 0.0)))
 (let (($x2826 (>= falcosecurity_hight 0.0)))
 (let (($x2825 (>= falcosecurity_width 0.0)))
 (let (($x2824 (>= falcosecurity_y 0.0)))
 (let (($x2823 (>= falcosecurity_x 0.0)))
 (let (($x2822 (>= explore_hight 0.0)))
 (let (($x2821 (>= explore_width 0.0)))
 (let (($x2820 (>= explore_y 0.0)))
 (let (($x2819 (>= explore_x 0.0)))
 (let (($x2818 (= (+ (- 30.0) last_changes_body_kid_8_hight) 0.0)))
 (let (($x2816 (= (+ (- 100.0) last_changes_body_kid_8_width) 0.0)))
 (let (($x2814 (= (+ (- 50.0) last_changes_body_kid_7_hight) 0.0)))
 (let (($x2812 (= (+ (- 300.0) last_changes_body_kid_7_width) 0.0)))
 (let (($x2810 (= (+ (- 30.0) last_changes_body_kid_6_hight) 0.0)))
 (let (($x2808 (= (+ (- 100.0) last_changes_body_kid_6_width) 0.0)))
 (let (($x2806 (= (+ (- 50.0) last_changes_body_kid_5_hight) 0.0)))
 (let (($x2804 (= (+ (- 300.0) last_changes_body_kid_5_width) 0.0)))
 (let (($x2802 (= (+ (- 30.0) last_changes_body_kid_4_hight) 0.0)))
 (let (($x2800 (= (+ (- 100.0) last_changes_body_kid_4_width) 0.0)))
 (let (($x2798 (= (+ (- 50.0) last_changes_body_kid_3_hight) 0.0)))
 (let (($x2796 (= (+ (- 300.0) last_changes_body_kid_3_width) 0.0)))
 (let (($x2794 (= (+ (- 30.0) last_changes_body_kid_2_hight) 0.0)))
 (let (($x2792 (= (+ (- 100.0) last_changes_body_kid_2_width) 0.0)))
 (let (($x2790 (= (+ (- 50.0) last_changes_body_kid_1_hight) 0.0)))
 (let (($x2788 (= (+ (- 300.0) last_changes_body_kid_1_width) 0.0)))
 (let (($x2786 (= (+ (- 30.0) last_changes_body_kid_0_hight) 0.0)))
 (let (($x2784 (= (+ (- 100.0) last_changes_body_kid_0_width) 0.0)))
 (let ((?x2746 (- (+ (- last_changes_body_kid_7_y) last_changes_body_kid_8_y) last_changes_body_kid_7_hight)))
 (let (($x2782 (or $x2572 (= ?x2746 10.0))))
 (let ((?x2742 (- (- last_changes_body_kid_7_y last_changes_body_kid_6_y) last_changes_body_kid_6_hight)))
 (let (($x2780 (or $x2572 (= ?x2742 10.0))))
 (let ((?x2738 (- (+ (- last_changes_body_kid_5_hight) last_changes_body_kid_6_y) last_changes_body_kid_5_y)))
 (let (($x2778 (or $x2572 (= ?x2738 10.0))))
 (let ((?x2648 (- (- last_changes_body_kid_4_y) last_changes_body_kid_4_hight)))
 (let ((?x2734 (+ ?x2648 last_changes_body_kid_5_y)))
 (let (($x2776 (or $x2572 (= ?x2734 10.0))))
 (let ((?x2731 (- (+ (- last_changes_body_kid_3_y) last_changes_body_kid_4_y) last_changes_body_kid_3_hight)))
 (let (($x2774 (or $x2572 (= ?x2731 10.0))))
 (let ((?x2727 (- (- last_changes_body_kid_3_y last_changes_body_kid_2_y) last_changes_body_kid_2_hight)))
 (let (($x2772 (or $x2572 (= ?x2727 10.0))))
 (let ((?x2723 (- (- last_changes_body_kid_2_y last_changes_body_kid_1_y) last_changes_body_kid_1_hight)))
 (let (($x2770 (or $x2572 (= ?x2723 10.0))))
 (let ((?x2719 (- (- last_changes_body_kid_1_y last_changes_body_kid_0_y) last_changes_body_kid_0_hight)))
 (let (($x2768 (or $x2572 (= ?x2719 10.0))))
 (let (($x2766 (or $x2572 (= (+ (- last_changes_body_x) last_changes_body_kid_8_x) 20.0))))
 (let (($x2764 (or $x2572 (= (+ (- last_changes_body_x) last_changes_body_kid_7_x) 20.0))))
 (let (($x2762 (or $x2572 (= (+ (- last_changes_body_x) last_changes_body_kid_6_x) 20.0))))
 (let (($x2760 (or $x2572 (= (+ (- last_changes_body_x) last_changes_body_kid_5_x) 20.0))))
 (let (($x2758 (or $x2572 (= (+ (- last_changes_body_x) last_changes_body_kid_4_x) 20.0))))
 (let (($x2756 (or $x2572 (= (+ (- last_changes_body_x) last_changes_body_kid_3_x) 20.0))))
 (let (($x2754 (or $x2572 (= (+ (- last_changes_body_x) last_changes_body_kid_2_x) 20.0))))
 (let (($x2752 (or $x2572 (= (+ (- last_changes_body_x) last_changes_body_kid_1_x) 20.0))))
 (let (($x2750 (or $x2572 (= (+ (- last_changes_body_x) last_changes_body_kid_0_x) 20.0))))
 (let (($x2748 (or $x2572 (>= ?x2746 0.0))))
 (let (($x2744 (or $x2572 (>= ?x2742 0.0))))
 (let (($x2740 (or $x2572 (>= ?x2738 0.0))))
 (let (($x2736 (or $x2572 (>= ?x2734 0.0))))
 (let (($x2733 (or $x2572 (>= ?x2731 0.0))))
 (let (($x2729 (or $x2572 (>= ?x2727 0.0))))
 (let (($x2725 (or $x2572 (>= ?x2723 0.0))))
 (let (($x2721 (or $x2572 (>= ?x2719 0.0))))
 (let ((?x2714 (- (+ (- last_changes_body_kid_8_y) last_changes_body_y) last_changes_body_kid_8_hight)))
 (let (($x2717 (or $x2572 (>= (+ ?x2714 last_changes_body_hight) 20.0))))
 (let (($x2711 (or $x2572 (>= (- last_changes_body_kid_8_y last_changes_body_y) 20.0))))
 (let ((?x2705 (+ (- last_changes_body_x last_changes_body_kid_8_width) last_changes_body_width)))
 (let (($x2708 (or $x2572 (>= (- ?x2705 last_changes_body_kid_8_x) 20.0))))
 (let (($x2703 (or $x2572 (>= (+ (- last_changes_body_x) last_changes_body_kid_8_x) 20.0))))
 (let ((?x2697 (+ (+ (- last_changes_body_kid_7_y) last_changes_body_y) last_changes_body_hight)))
 (let (($x2700 (or $x2572 (>= (- ?x2697 last_changes_body_kid_7_hight) 20.0))))
 (let (($x2694 (or $x2572 (>= (- last_changes_body_kid_7_y last_changes_body_y) 20.0))))
 (let ((?x2521 (+ last_changes_body_x last_changes_body_width)))
 (let (($x2690 (>= (- (- ?x2521 last_changes_body_kid_7_width) last_changes_body_kid_7_x) 20.0)))
 (let (($x2691 (or $x2572 $x2690)))
 (let (($x2687 (or $x2572 (>= (+ (- last_changes_body_x) last_changes_body_kid_7_x) 20.0))))
 (let ((?x2681 (+ (- last_changes_body_y last_changes_body_kid_6_y) last_changes_body_hight)))
 (let (($x2684 (or $x2572 (>= (- ?x2681 last_changes_body_kid_6_hight) 20.0))))
 (let (($x2679 (or $x2572 (>= (+ (- last_changes_body_y) last_changes_body_kid_6_y) 20.0))))
 (let ((?x2673 (+ (- last_changes_body_x last_changes_body_kid_6_x) last_changes_body_width)))
 (let (($x2676 (or $x2572 (>= (- ?x2673 last_changes_body_kid_6_width) 20.0))))
 (let (($x2671 (or $x2572 (>= (+ (- last_changes_body_x) last_changes_body_kid_6_x) 20.0))))
 (let ((?x2665 (+ (+ (- last_changes_body_kid_5_hight) last_changes_body_y) last_changes_body_hight)))
 (let (($x2668 (or $x2572 (>= (- ?x2665 last_changes_body_kid_5_y) 20.0))))
 (let (($x2662 (or $x2572 (>= (+ (- last_changes_body_y) last_changes_body_kid_5_y) 20.0))))
 (let (($x2658 (>= (- (- ?x2521 last_changes_body_kid_5_x) last_changes_body_kid_5_width) 20.0)))
 (let (($x2659 (or $x2572 $x2658)))
 (let (($x2655 (or $x2572 (>= (+ (- last_changes_body_x) last_changes_body_kid_5_x) 20.0))))
 (let (($x2652 (or $x2572 (>= (+ (+ ?x2648 last_changes_body_y) last_changes_body_hight) 20.0))))
 (let (($x2646 (or $x2572 (>= (- last_changes_body_kid_4_y last_changes_body_y) 20.0))))
 (let (($x2642 (>= (- (- ?x2521 last_changes_body_kid_4_x) last_changes_body_kid_4_width) 20.0)))
 (let (($x2643 (or $x2572 $x2642)))
 (let (($x2639 (or $x2572 (>= (+ (- last_changes_body_x) last_changes_body_kid_4_x) 20.0))))
 (let ((?x2633 (+ (- (- last_changes_body_kid_3_y) last_changes_body_kid_3_hight) last_changes_body_y)))
 (let (($x2636 (or $x2572 (>= (+ ?x2633 last_changes_body_hight) 20.0))))
 (let (($x2630 (or $x2572 (>= (- last_changes_body_kid_3_y last_changes_body_y) 20.0))))
 (let (($x2626 (>= (- (- ?x2521 last_changes_body_kid_3_x) last_changes_body_kid_3_width) 20.0)))
 (let (($x2627 (or $x2572 $x2626)))
 (let (($x2623 (or $x2572 (>= (+ (- last_changes_body_x) last_changes_body_kid_3_x) 20.0))))
 (let ((?x2617 (+ (- (- last_changes_body_kid_2_y) last_changes_body_kid_2_hight) last_changes_body_y)))
 (let (($x2620 (or $x2572 (>= (+ ?x2617 last_changes_body_hight) 20.0))))
 (let (($x2614 (or $x2572 (>= (- last_changes_body_kid_2_y last_changes_body_y) 20.0))))
 (let (($x2610 (>= (- (- ?x2521 last_changes_body_kid_2_x) last_changes_body_kid_2_width) 20.0)))
 (let (($x2611 (or $x2572 $x2610)))
 (let (($x2607 (or $x2572 (>= (+ (- last_changes_body_x) last_changes_body_kid_2_x) 20.0))))
 (let ((?x2601 (- (+ (- last_changes_body_kid_1_y) last_changes_body_y) last_changes_body_kid_1_hight)))
 (let (($x2604 (or $x2572 (>= (+ ?x2601 last_changes_body_hight) 20.0))))
 (let (($x2598 (or $x2572 (>= (- last_changes_body_kid_1_y last_changes_body_y) 20.0))))
 (let ((?x2592 (+ (- last_changes_body_x last_changes_body_kid_1_width) last_changes_body_width)))
 (let (($x2595 (or $x2572 (>= (- ?x2592 last_changes_body_kid_1_x) 20.0))))
 (let (($x2590 (or $x2572 (>= (+ (- last_changes_body_x) last_changes_body_kid_1_x) 20.0))))
 (let ((?x2584 (+ (- last_changes_body_y last_changes_body_kid_0_y) last_changes_body_hight)))
 (let (($x2587 (or $x2572 (>= (- ?x2584 last_changes_body_kid_0_hight) 20.0))))
 (let (($x2582 (or $x2572 (>= (+ (- last_changes_body_y) last_changes_body_kid_0_y) 20.0))))
 (let (($x2578 (>= (- (- ?x2521 last_changes_body_kid_0_width) last_changes_body_kid_0_x) 20.0)))
 (let (($x2579 (or $x2572 $x2578)))
 (let (($x2575 (or $x2572 (>= (+ (- last_changes_body_x) last_changes_body_kid_0_x) 20.0))))
 (let (($x2571 (>= last_changes_body_kid_8_hight 0.0)))
 (let (($x2570 (>= last_changes_body_kid_8_width 0.0)))
 (let (($x2569 (>= last_changes_body_kid_8_y 0.0)))
 (let (($x2568 (>= last_changes_body_kid_8_x 0.0)))
 (let (($x2567 (>= last_changes_body_kid_7_hight 0.0)))
 (let (($x2566 (>= last_changes_body_kid_7_width 0.0)))
 (let (($x2565 (>= last_changes_body_kid_7_y 0.0)))
 (let (($x2564 (>= last_changes_body_kid_7_x 0.0)))
 (let (($x2563 (>= last_changes_body_kid_6_hight 0.0)))
 (let (($x2562 (>= last_changes_body_kid_6_width 0.0)))
 (let (($x2561 (>= last_changes_body_kid_6_y 0.0)))
 (let (($x2560 (>= last_changes_body_kid_6_x 0.0)))
 (let (($x2559 (>= last_changes_body_kid_5_hight 0.0)))
 (let (($x2558 (>= last_changes_body_kid_5_width 0.0)))
 (let (($x2557 (>= last_changes_body_kid_5_y 0.0)))
 (let (($x2556 (>= last_changes_body_kid_5_x 0.0)))
 (let (($x2555 (>= last_changes_body_kid_4_hight 0.0)))
 (let (($x2554 (>= last_changes_body_kid_4_width 0.0)))
 (let (($x2553 (>= last_changes_body_kid_4_y 0.0)))
 (let (($x2552 (>= last_changes_body_kid_4_x 0.0)))
 (let (($x2551 (>= last_changes_body_kid_3_hight 0.0)))
 (let (($x2550 (>= last_changes_body_kid_3_width 0.0)))
 (let (($x2549 (>= last_changes_body_kid_3_y 0.0)))
 (let (($x2548 (>= last_changes_body_kid_3_x 0.0)))
 (let (($x2547 (>= last_changes_body_kid_2_hight 0.0)))
 (let (($x2546 (>= last_changes_body_kid_2_width 0.0)))
 (let (($x2545 (>= last_changes_body_kid_2_y 0.0)))
 (let (($x2544 (>= last_changes_body_kid_2_x 0.0)))
 (let (($x2543 (>= last_changes_body_kid_1_hight 0.0)))
 (let (($x2542 (>= last_changes_body_kid_1_width 0.0)))
 (let (($x2541 (>= last_changes_body_kid_1_y 0.0)))
 (let (($x2540 (>= last_changes_body_kid_1_x 0.0)))
 (let (($x2539 (>= last_changes_body_kid_0_hight 0.0)))
 (let (($x2538 (>= last_changes_body_kid_0_width 0.0)))
 (let (($x2537 (>= last_changes_body_kid_0_y 0.0)))
 (let (($x2536 (>= last_changes_body_kid_0_x 0.0)))
 (let (($x2535 (or $x2470 (= last_changes_title_hight 50.0))))
 (let ((?x2509 (- (+ (- last_changes_title_hight) last_changes_body_y) last_changes_title_y)))
 (let (($x2533 (or $x2470 (= ?x2509 20.0))))
 (let ((?x2529 (- (+ (- last_changes_body_y last_changes_y) last_changes_body_hight) last_changes_hight)))
 (let (($x2531 (or $x2470 (= ?x2529 (- 20.0)))))
 (let (($x2527 (or $x2470 (= (+ (- last_changes_y) last_changes_title_y) 20.0))))
 (let (($x2525 (or $x2470 (= (- (- ?x2521 last_changes_width) last_changes_x) (- 20.0)))))
 (let ((?x2517 (+ (- last_changes_title_x last_changes_width) last_changes_title_width)))
 (let (($x2520 (or $x2470 (= (- ?x2517 last_changes_x) (- 20.0)))))
 (let (($x2515 (or $x2470 (= (- last_changes_body_x last_changes_x) 20.0))))
 (let (($x2513 (or $x2470 (= (- last_changes_title_x last_changes_x) 20.0))))
 (let (($x2511 (or $x2470 (>= ?x2509 0.0))))
 (let ((?x2504 (- (+ (- last_changes_body_y) last_changes_y) last_changes_body_hight)))
 (let (($x2507 (or $x2470 (>= (+ ?x2504 last_changes_hight) 0.0))))
 (let (($x2501 (or $x2470 (>= (- last_changes_body_y last_changes_y) 0.0))))
 (let ((?x2495 (+ (- (- last_changes_body_x) last_changes_body_width) last_changes_width)))
 (let (($x2498 (or $x2470 (>= (+ ?x2495 last_changes_x) 0.0))))
 (let (($x2492 (or $x2470 (>= (- last_changes_body_x last_changes_x) 0.0))))
 (let ((?x2486 (- (+ (- last_changes_title_hight) last_changes_y) last_changes_title_y)))
 (let (($x2489 (or $x2470 (>= (+ ?x2486 last_changes_hight) 0.0))))
 (let (($x2483 (or $x2470 (>= (+ (- last_changes_y) last_changes_title_y) 0.0))))
 (let ((?x2476 (- (+ (- last_changes_title_x) last_changes_width) last_changes_title_width)))
 (let (($x2479 (or $x2470 (>= (+ ?x2476 last_changes_x) 0.0))))
 (let (($x2473 (or $x2470 (>= (- last_changes_title_x last_changes_x) 0.0))))
 (let (($x2469 (>= last_changes_body_hight 0.0)))
 (let (($x2468 (>= last_changes_body_width 0.0)))
 (let (($x2467 (>= last_changes_body_y 0.0)))
 (let (($x2466 (>= last_changes_body_x 0.0)))
 (let (($x2465 (>= last_changes_title_hight 0.0)))
 (let (($x2464 (>= last_changes_title_width 0.0)))
 (let (($x2463 (>= last_changes_title_y 0.0)))
 (let (($x2462 (>= last_changes_title_x 0.0)))
 (let (($x2461 (= (+ (- 200.0) the_state_of_oct_hight) 0.0)))
 (let (($x2458 (= (+ (- the_state_of_oct_kid_2_hight) the_state_of_oct_kid_0_hight) 0.0)))
 (let (($x2459 (or $x2364 $x2458)))
 (let (($x2454 (= (- the_state_of_oct_kid_0_hight the_state_of_oct_kid_1_hight) 0.0)))
 (let (($x2455 (or $x2364 $x2454)))
 (let ((?x2449 (- (+ the_state_of_oct_kid_2_y the_state_of_oct_kid_2_hight) the_state_of_oct_y)))
 (let (($x2452 (or $x2364 (= (- ?x2449 the_state_of_oct_hight) (- 20.0)))))
 (let (($x2447 (or $x2364 (= (- the_state_of_oct_kid_0_y the_state_of_oct_y) 20.0))))
 (let ((?x2365 (- the_state_of_oct_x)))
 (let ((?x2433 (- ?x2365 the_state_of_oct_width)))
 (let (($x2444 (= (+ (+ ?x2433 the_state_of_oct_kid_2_x) the_state_of_oct_kid_2_width) (- 20.0))))
 (let (($x2445 (or $x2364 $x2444)))
 (let (($x2440 (= (+ (+ ?x2433 the_state_of_oct_kid_1_x) the_state_of_oct_kid_1_width) (- 20.0))))
 (let (($x2441 (or $x2364 $x2440)))
 (let (($x2436 (= (+ (+ ?x2433 the_state_of_oct_kid_0_x) the_state_of_oct_kid_0_width) (- 20.0))))
 (let (($x2437 (or $x2364 $x2436)))
 (let (($x2432 (or $x2364 (= (+ ?x2365 the_state_of_oct_kid_2_x) 20.0))))
 (let (($x2430 (or $x2364 (= (+ ?x2365 the_state_of_oct_kid_1_x) 20.0))))
 (let (($x2428 (or $x2364 (= (+ ?x2365 the_state_of_oct_kid_0_x) 20.0))))
 (let ((?x2420 (- (+ (- the_state_of_oct_kid_1_y) the_state_of_oct_kid_2_y) the_state_of_oct_kid_1_hight)))
 (let (($x2426 (or $x2364 (= ?x2420 20.0))))
 (let ((?x2416 (- (- the_state_of_oct_kid_1_y the_state_of_oct_kid_0_y) the_state_of_oct_kid_0_hight)))
 (let (($x2424 (or $x2364 (= ?x2416 20.0))))
 (let (($x2422 (or $x2364 (>= ?x2420 0.0))))
 (let (($x2418 (or $x2364 (>= ?x2416 0.0))))
 (let ((?x2411 (+ (- (- the_state_of_oct_kid_2_y) the_state_of_oct_kid_2_hight) the_state_of_oct_y)))
 (let (($x2414 (or $x2364 (>= (+ ?x2411 the_state_of_oct_hight) 0.0))))
 (let (($x2408 (or $x2364 (>= (- the_state_of_oct_kid_2_y the_state_of_oct_y) 0.0))))
 (let ((?x2369 (+ the_state_of_oct_x the_state_of_oct_width)))
 (let (($x2404 (>= (- (- ?x2369 the_state_of_oct_kid_2_x) the_state_of_oct_kid_2_width) 0.0)))
 (let (($x2405 (or $x2364 $x2404)))
 (let (($x2401 (or $x2364 (>= (+ ?x2365 the_state_of_oct_kid_2_x) 0.0))))
 (let ((?x2395 (+ (- (- the_state_of_oct_kid_1_y) the_state_of_oct_kid_1_hight) the_state_of_oct_y)))
 (let (($x2398 (or $x2364 (>= (+ ?x2395 the_state_of_oct_hight) 0.0))))
 (let (($x2392 (or $x2364 (>= (- the_state_of_oct_kid_1_y the_state_of_oct_y) 0.0))))
 (let (($x2388 (>= (- (- ?x2369 the_state_of_oct_kid_1_x) the_state_of_oct_kid_1_width) 0.0)))
 (let (($x2389 (or $x2364 $x2388)))
 (let (($x2385 (or $x2364 (>= (+ ?x2365 the_state_of_oct_kid_1_x) 0.0))))
 (let ((?x2379 (+ (- (- the_state_of_oct_kid_0_y) the_state_of_oct_kid_0_hight) the_state_of_oct_y)))
 (let (($x2382 (or $x2364 (>= (+ ?x2379 the_state_of_oct_hight) 0.0))))
 (let (($x2376 (or $x2364 (>= (- the_state_of_oct_kid_0_y the_state_of_oct_y) 0.0))))
 (let (($x2372 (>= (- (- ?x2369 the_state_of_oct_kid_0_x) the_state_of_oct_kid_0_width) 0.0)))
 (let (($x2373 (or $x2364 $x2372)))
 (let (($x2368 (or $x2364 (>= (+ ?x2365 the_state_of_oct_kid_0_x) 0.0))))
 (let (($x2363 (>= the_state_of_oct_kid_2_hight 0.0)))
 (let (($x2362 (>= the_state_of_oct_kid_2_width 0.0)))
 (let (($x2361 (>= the_state_of_oct_kid_2_y 0.0)))
 (let (($x2360 (>= the_state_of_oct_kid_2_x 0.0)))
 (let (($x2359 (>= the_state_of_oct_kid_1_hight 0.0)))
 (let (($x2358 (>= the_state_of_oct_kid_1_width 0.0)))
 (let (($x2357 (>= the_state_of_oct_kid_1_y 0.0)))
 (let (($x2356 (>= the_state_of_oct_kid_1_x 0.0)))
 (let (($x2355 (>= the_state_of_oct_kid_0_hight 0.0)))
 (let (($x2354 (>= the_state_of_oct_kid_0_width 0.0)))
 (let (($x2353 (>= the_state_of_oct_kid_0_y 0.0)))
 (let (($x2352 (>= the_state_of_oct_kid_0_x 0.0)))
 (let ((?x1435 (- right_2_collom_y)))
 (let ((?x1453 (+ ?x1435 right_homes_y)))
 (let (($x2351 (= ?x1453 0.0)))
 (let ((?x2349 (- (- (+ right_homes_x right_homes_width) right_2_collom_x) right_2_collom_width)))
 (let (($x2350 (= ?x2349 0.0)))
 (let (($x2347 (= (+ (- 400.0) right_homes_width) 0.0)))
 (let (($x2344 (or $x2256 (= (- (- explore_repo_y last_changes_y) last_changes_hight) 20.0))))
 (let ((?x2334 (- (+ (- the_state_of_oct_y) last_changes_y) the_state_of_oct_hight)))
 (let (($x2342 (or $x2256 (= ?x2334 20.0))))
 (let ((?x2338 (- (- explore_repo_y last_changes_y) last_changes_hight)))
 (let (($x2340 (or $x2256 (>= ?x2338 0.0))))
 (let (($x2336 (or $x2256 (>= ?x2334 0.0))))
 (let ((?x2329 (+ (- (+ (- explore_repo_y) right_homes_y) explore_repo_hight) right_homes_hight)))
 (let (($x2331 (or $x2256 (>= ?x2329 0.0))))
 (let (($x2325 (or $x2256 (>= (- explore_repo_y right_homes_y) 0.0))))
 (let ((?x2321 (- (+ (- right_homes_x explore_repo_width) right_homes_width) explore_repo_x)))
 (let (($x2323 (or $x2256 (>= ?x2321 0.0))))
 (let (($x2318 (or $x2256 (>= (+ (- right_homes_x) explore_repo_x) 0.0))))
 (let ((?x2314 (- (+ (- right_homes_y last_changes_y) right_homes_hight) last_changes_hight)))
 (let (($x2316 (or $x2256 (>= ?x2314 0.0))))
 (let (($x2311 (or $x2256 (>= (+ (- right_homes_y) last_changes_y) 0.0))))
 (let ((?x2306 (- (- (+ right_homes_x right_homes_width) last_changes_width) last_changes_x)))
 (let (($x2308 (or $x2256 (>= ?x2306 0.0))))
 (let (($x2303 (or $x2256 (>= (+ (- right_homes_x) last_changes_x) 0.0))))
 (let ((?x2299 (- (+ (- right_homes_y the_state_of_oct_y) right_homes_hight) the_state_of_oct_hight)))
 (let (($x2301 (or $x2256 (>= ?x2299 0.0))))
 (let (($x2296 (or $x2256 (>= (+ (- right_homes_y) the_state_of_oct_y) 0.0))))
 (let ((?x2292 (- (+ (- right_homes_x the_state_of_oct_x) right_homes_width) the_state_of_oct_width)))
 (let (($x2294 (or $x2256 (>= ?x2292 0.0))))
 (let (($x2289 (or $x2256 (>= (+ (- right_homes_x) the_state_of_oct_x) 0.0))))
 (let ((?x2285 (- (+ (- explore_repo_y right_homes_y) explore_repo_hight) right_homes_hight)))
 (let (($x2287 (or $x2256 (= ?x2285 0.0))))
 (let (($x2282 (or $x2256 (= (+ (- right_homes_y) the_state_of_oct_y) 0.0))))
 (let ((?x2276 (+ (- (+ (- right_homes_x) explore_repo_width) right_homes_width) explore_repo_x)))
 (let (($x2278 (or $x2256 (= ?x2276 0.0))))
 (let ((?x2271 (+ (+ (- (- right_homes_x) right_homes_width) last_changes_width) last_changes_x)))
 (let (($x2273 (or $x2256 (= ?x2271 0.0))))
 (let ((?x2267 (+ (- (+ (- right_homes_x) the_state_of_oct_x) right_homes_width) the_state_of_oct_width)))
 (let (($x2269 (or $x2256 (= ?x2267 0.0))))
 (let (($x2265 (or $x2256 (= (+ (- right_homes_x) explore_repo_x) 0.0))))
 (let (($x2262 (or $x2256 (= (+ (- right_homes_x) last_changes_x) 0.0))))
 (let (($x2259 (or $x2256 (= (+ (- right_homes_x) the_state_of_oct_x) 0.0))))
 (let (($x2255 (>= explore_repo_hight 0.0)))
 (let (($x2254 (>= explore_repo_width 0.0)))
 (let (($x2253 (>= explore_repo_y 0.0)))
 (let (($x2252 (>= explore_repo_x 0.0)))
 (let (($x2251 (>= last_changes_hight 0.0)))
 (let (($x2250 (>= last_changes_width 0.0)))
 (let (($x2249 (>= last_changes_y 0.0)))
 (let (($x2248 (>= last_changes_x 0.0)))
 (let (($x2247 (>= the_state_of_oct_hight 0.0)))
 (let (($x2246 (>= the_state_of_oct_width 0.0)))
 (let (($x2245 (>= the_state_of_oct_y 0.0)))
 (let (($x2244 (>= the_state_of_oct_x 0.0)))
 (let ((?x2241 (+ (- (+ (- rec_hight) rec_right_icon_hight) rec_y) rec_right_icon_y)))
 (let (($x2243 (or $x2144 (= ?x2241 (- 20.0)))))
 (let (($x2238 (= (+ (- 50.0) rec_right_icon_hight) 0.0)))
 (let (($x2236 (= (+ (- 50.0) rec_right_icon_width) 0.0)))
 (let (($x2233 (= (+ (- (- (- 20.0) rec_word_y) rec_word_hight) rec_right_icon_y) 0.0)))
 (let (($x2234 (or $x2144 $x2233)))
 (let ((?x2228 (- (- (+ (- 20.0) rec_right_icon_x) rec_left_icon_x) rec_left_icon_width)))
 (let (($x2230 (or $x2144 (= ?x2228 0.0))))
 (let (($x2225 (>= rec_right_icon_hight 0.0)))
 (let (($x2224 (>= rec_right_icon_width 0.0)))
 (let (($x2223 (>= rec_right_icon_y 0.0)))
 (let (($x2222 (>= rec_right_icon_x 0.0)))
 (let (($x2221 (= (+ (- 50.0) rec_left_icon_hight) 0.0)))
 (let (($x2219 (= (+ (- 50.0) rec_left_icon_width) 0.0)))
 (let (($x2216 (= (- (+ (- (- 20.0) rec_word_y) rec_left_icon_y) rec_word_hight) 0.0)))
 (let (($x2217 (or $x2144 $x2216)))
 (let (($x2212 (or $x2144 (= (+ (- rec_x) rec_left_icon_x) 20.0))))
 (let (($x2209 (>= rec_left_icon_hight 0.0)))
 (let (($x2208 (>= rec_left_icon_width 0.0)))
 (let (($x2207 (>= rec_left_icon_y 0.0)))
 (let (($x2206 (>= rec_left_icon_x 0.0)))
 (let (($x2205 (or $x2144 (= (- (- (+ (- 20.0) rec_word_y) boolect_y) boolect_hight) 0.0))))
 (let (($x2200 (= (+ (- 200.0) rec_word_hight) 0.0)))
 (let (($x2197 (= (+ (+ (- (- rec_x) rec_width) rec_word_x) rec_word_width) (- 20.0))))
 (let (($x2198 (or $x2144 $x2197)))
 (let (($x2194 (or $x2144 (= (+ (- rec_x) rec_word_x) 20.0))))
 (let (($x2191 (>= rec_word_hight 0.0)))
 (let (($x2190 (>= rec_word_width 0.0)))
 (let (($x2189 (>= rec_word_y 0.0)))
 (let (($x2188 (>= rec_word_x 0.0)))
 (let (($x2187 (= (+ (- 100.0) stars_width) 0.0)))
 (let (($x2185 (or $x2144 (= (- stars_hight boolect_hight) 0.0))))
 (let (($x2182 (or $x2144 (= (- stars_y boolect_y) 0.0))))
 (let (($x2179 (or $x2144 (= (+ (+ (- (- rec_x) rec_width) stars_x) stars_width) (- 20.0)))))
 (let (($x2174 (>= stars_hight 0.0)))
 (let (($x2173 (>= stars_width 0.0)))
 (let (($x2172 (>= stars_y 0.0)))
 (let (($x2171 (>= stars_x 0.0)))
 (let ((?x2168 (- (- (+ (- 20.0) boolect_y) recomend_for_you_y) recomend_for_you_hight)))
 (let (($x2170 (or $x2144 (= ?x2168 0.0))))
 (let (($x2165 (or $x2144 (= (+ (- rec_x) boolect_x) 20.0))))
 (let (($x2162 (= (+ (- 50.0) boolect_hight) 0.0)))
 (let (($x2160 (= (+ (- 100.0) boolect_width) 0.0)))
 (let (($x2158 (>= boolect_hight 0.0)))
 (let (($x2157 (>= boolect_width 0.0)))
 (let (($x2156 (>= boolect_y 0.0)))
 (let (($x2155 (>= boolect_x 0.0)))
 (let (($x2154 (= (+ (- 50.0) recomend_for_you_hight) 0.0)))
 (let (($x2152 (= (+ (- 100.0) recomend_for_you_width) 0.0)))
 (let (($x2150 (or $x2144 (= (- recomend_for_you_y rec_y) 20.0))))
 (let (($x2147 (or $x2144 (= (- recomend_for_you_x rec_x) 20.0))))
 (let (($x2143 (>= recomend_for_you_hight 0.0)))
 (let (($x2142 (>= recomend_for_you_width 0.0)))
 (let (($x2141 (>= recomend_for_you_y 0.0)))
 (let (($x2140 (>= recomend_for_you_x 0.0)))
 (let (($x2139 (= (+ (- 50.0) cvc_smile_hight) 0.0)))
 (let (($x2137 (= (+ (- 50.0) cvc_smile_width) 0.0)))
 (let ((?x2133 (+ (+ (- (- cvc_page_y) cvc_page_hight) cvc_smile_y) cvc_smile_hight)))
 (let (($x2135 (or $x2020 (= ?x2133 (- 20.0)))))
 (let ((?x2129 (- (+ (- cvc_changes_x cvc_page_x) cvc_changes_width) cvc_page_width)))
 (let (($x2131 (or $x2020 (= ?x2129 (- 20.0)))))
 (let (($x2127 (= (+ (- 200.0) cvc_changes_hight) 0.0)))
 (let (($x2125 (= (+ (- 50.0) cvc_version_hight) 0.0)))
 (let (($x2123 (= (+ (- 100.0) cvc_version_width) 0.0)))
 (let (($x2121 (= (+ (- 50.0) cvc_icon_hight) 0.0)))
 (let (($x2119 (= (+ (- 150.0) cvc_icon_width) 0.0)))
 (let (($x2117 (or $x2020 (= (- cvc_smile_x cvc_page_x) 20.0))))
 (let (($x2115 (or $x2020 (= (- cvc_changes_x cvc_page_x) 20.0))))
 (let (($x2113 (or $x2020 (= (+ (- cvc_page_x) cvc_version_x) 20.0))))
 (let (($x2111 (or $x2020 (= (+ (- cvc_page_x) cvc_icon_x) 20.0))))
 (let ((?x2033 (- (+ (- cvc_changes_hight) cvc_smile_y) cvc_changes_y)))
 (let (($x2109 (or $x2020 (>= ?x2033 0.0))))
 (let ((?x2028 (+ (- (- cvc_version_y) cvc_version_hight) cvc_changes_y)))
 (let (($x2107 (or $x2020 (>= ?x2028 0.0))))
 (let (($x2105 (or $x2020 (>= (- (+ (- cvc_icon_y) cvc_version_y) cvc_icon_hight) 0.0))))
 (let (($x2102 (>= (- (- (+ cvc_page_y cvc_page_hight) cvc_smile_y) cvc_smile_hight) 20.0)))
 (let (($x2103 (or $x2020 $x2102)))
 (let (($x2098 (or $x2020 (>= (+ (- cvc_page_y) cvc_smile_y) 20.0))))
 (let ((?x2093 (+ (+ (- (- cvc_smile_x) cvc_smile_width) cvc_page_x) cvc_page_width)))
 (let (($x2095 (or $x2020 (>= ?x2093 20.0))))
 (let (($x2089 (or $x2020 (>= (- cvc_smile_x cvc_page_x) 20.0))))
 (let ((?x2084 (- (+ (- cvc_page_y cvc_changes_hight) cvc_page_hight) cvc_changes_y)))
 (let (($x2086 (or $x2020 (>= ?x2084 20.0))))
 (let (($x2081 (or $x2020 (>= (+ (- cvc_page_y) cvc_changes_y) 20.0))))
 (let ((?x2076 (+ (- (+ (- cvc_changes_x) cvc_page_x) cvc_changes_width) cvc_page_width)))
 (let (($x2078 (or $x2020 (>= ?x2076 20.0))))
 (let (($x2072 (or $x2020 (>= (- cvc_changes_x cvc_page_x) 20.0))))
 (let ((?x2067 (- (+ (- cvc_page_y cvc_version_y) cvc_page_hight) cvc_version_hight)))
 (let (($x2069 (or $x2020 (>= ?x2067 20.0))))
 (let (($x2064 (or $x2020 (>= (+ (- cvc_page_y) cvc_version_y) 20.0))))
 (let ((?x2059 (- (+ (- cvc_page_x cvc_version_x) cvc_page_width) cvc_version_width)))
 (let (($x2061 (or $x2020 (>= ?x2059 20.0))))
 (let (($x2056 (or $x2020 (>= (+ (- cvc_page_x) cvc_version_x) 20.0))))
 (let (($x2052 (>= (- (+ (- cvc_page_y cvc_icon_y) cvc_page_hight) cvc_icon_hight) 20.0)))
 (let (($x2053 (or $x2020 $x2052)))
 (let (($x2048 (or $x2020 (>= (+ (- cvc_page_y) cvc_icon_y) 20.0))))
 (let ((?x2043 (+ (- (+ (- cvc_icon_width) cvc_page_x) cvc_icon_x) cvc_page_width)))
 (let (($x2045 (or $x2020 (>= ?x2043 20.0))))
 (let (($x2039 (or $x2020 (>= (+ (- cvc_page_x) cvc_icon_x) 20.0))))
 (let (($x2035 (or $x2020 (= ?x2033 20.0))))
 (let (($x2030 (or $x2020 (= ?x2028 20.0))))
 (let (($x2025 (or $x2020 (= (- (+ (- cvc_icon_y) cvc_version_y) cvc_icon_hight) 20.0))))
 (let (($x2019 (>= cvc_smile_hight 0.0)))
 (let (($x2018 (>= cvc_smile_width 0.0)))
 (let (($x2017 (>= cvc_smile_y 0.0)))
 (let (($x2016 (>= cvc_smile_x 0.0)))
 (let (($x2015 (>= cvc_changes_hight 0.0)))
 (let (($x2014 (>= cvc_changes_width 0.0)))
 (let (($x2013 (>= cvc_changes_y 0.0)))
 (let (($x2012 (>= cvc_changes_x 0.0)))
 (let (($x2011 (>= cvc_version_hight 0.0)))
 (let (($x2010 (>= cvc_version_width 0.0)))
 (let (($x2009 (>= cvc_version_y 0.0)))
 (let (($x2008 (>= cvc_version_x 0.0)))
 (let (($x2007 (>= cvc_icon_hight 0.0)))
 (let (($x2006 (>= cvc_icon_width 0.0)))
 (let (($x2005 (>= cvc_icon_y 0.0)))
 (let (($x2004 (>= cvc_icon_x 0.0)))
 (let (($x2003 (= (+ (- 50.0) z3_smile_hight) 0.0)))
 (let (($x2001 (= (+ (- 50.0) z3_smile_width) 0.0)))
 (let ((?x1997 (+ (- (+ (- z3_page_y) z3_smile_y) z3_page_hight) z3_smile_hight)))
 (let (($x1999 (or $x1882 (= ?x1997 (- 20.0)))))
 (let (($x1994 (= (+ (- (- changes_width z3_page_x) z3_page_width) changes_x) (- 20.0))))
 (let (($x1995 (or $x1882 $x1994)))
 (let (($x1990 (= (+ (- 200.0) changes_hight) 0.0)))
 (let (($x1988 (= (+ (- 50.0) z3_version_hight) 0.0)))
 (let (($x1986 (= (+ (- 100.0) z3_version_width) 0.0)))
 (let (($x1984 (= (+ (- 50.0) z3_icon_hight) 0.0)))
 (let (($x1982 (= (+ (- 150.0) z3_icon_width) 0.0)))
 (let (($x1979 (or $x1882 (= (+ (- z3_page_x) z3_smile_x) 20.0))))
 (let (($x1977 (or $x1882 (= (+ (- z3_page_x) changes_x) 20.0))))
 (let (($x1975 (or $x1882 (= (- z3_version_x z3_page_x) 20.0))))
 (let (($x1973 (or $x1882 (= (- z3_icon_x z3_page_x) 20.0))))
 (let (($x1971 (or $x1882 (>= (- (- z3_smile_y changes_y) changes_hight) 0.0))))
 (let (($x1969 (or $x1882 (>= (- (+ (- z3_version_hight) changes_y) z3_version_y) 0.0))))
 (let (($x1967 (or $x1882 (>= (+ (- (- z3_icon_hight) z3_icon_y) z3_version_y) 0.0))))
 (let (($x1964 (>= (- (+ (- z3_page_y z3_smile_y) z3_page_hight) z3_smile_hight) 20.0)))
 (let (($x1965 (or $x1882 $x1964)))
 (let (($x1960 (or $x1882 (>= (+ (- z3_page_y) z3_smile_y) 20.0))))
 (let (($x1956 (>= (- (+ (- z3_page_x z3_smile_x) z3_page_width) z3_smile_width) 20.0)))
 (let (($x1957 (or $x1882 $x1956)))
 (let (($x1952 (or $x1882 (>= (+ (- z3_page_x) z3_smile_x) 20.0))))
 (let (($x1948 (>= (- (- (+ z3_page_y z3_page_hight) changes_y) changes_hight) 20.0)))
 (let (($x1949 (or $x1882 $x1948)))
 (let (($x1944 (or $x1882 (>= (+ (- z3_page_y) changes_y) 20.0))))
 (let (($x1940 (>= (- (+ (+ (- changes_width) z3_page_x) z3_page_width) changes_x) 20.0)))
 (let (($x1941 (or $x1882 $x1940)))
 (let (($x1935 (or $x1882 (>= (+ (- z3_page_x) changes_x) 20.0))))
 (let ((?x1929 (- (+ (+ (- z3_version_hight) z3_page_y) z3_page_hight) z3_version_y)))
 (let (($x1931 (or $x1882 (>= ?x1929 20.0))))
 (let (($x1926 (or $x1882 (>= (+ (- z3_page_y) z3_version_y) 20.0))))
 (let ((?x1921 (+ (+ (- (- z3_version_x) z3_version_width) z3_page_x) z3_page_width)))
 (let (($x1923 (or $x1882 (>= ?x1921 20.0))))
 (let (($x1917 (or $x1882 (>= (- z3_version_x z3_page_x) 20.0))))
 (let (($x1913 (>= (- (+ (+ (- z3_icon_hight) z3_page_y) z3_page_hight) z3_icon_y) 20.0)))
 (let (($x1914 (or $x1882 $x1913)))
 (let (($x1909 (or $x1882 (>= (+ (- z3_page_y) z3_icon_y) 20.0))))
 (let (($x1904 (>= (+ (+ (- (- z3_icon_x) z3_icon_width) z3_page_x) z3_page_width) 20.0)))
 (let (($x1905 (or $x1882 $x1904)))
 (let (($x1899 (or $x1882 (>= (- z3_icon_x z3_page_x) 20.0))))
 (let (($x1896 (or $x1882 (= (- (- z3_smile_y changes_y) changes_hight) 20.0))))
 (let (($x1892 (or $x1882 (= (- (+ (- z3_version_hight) changes_y) z3_version_y) 20.0))))
 (let (($x1887 (or $x1882 (= (+ (- (- z3_icon_hight) z3_icon_y) z3_version_y) 20.0))))
 (let (($x1881 (>= z3_smile_hight 0.0)))
 (let (($x1880 (>= z3_smile_width 0.0)))
 (let (($x1879 (>= z3_smile_y 0.0)))
 (let (($x1878 (>= z3_smile_x 0.0)))
 (let (($x1877 (>= changes_hight 0.0)))
 (let (($x1876 (>= changes_width 0.0)))
 (let (($x1875 (>= changes_y 0.0)))
 (let (($x1874 (>= changes_x 0.0)))
 (let (($x1873 (>= z3_version_hight 0.0)))
 (let (($x1872 (>= z3_version_width 0.0)))
 (let (($x1871 (>= z3_version_y 0.0)))
 (let (($x1870 (>= z3_version_x 0.0)))
 (let (($x1869 (>= z3_icon_hight 0.0)))
 (let (($x1868 (>= z3_icon_width 0.0)))
 (let (($x1867 (>= z3_icon_y 0.0)))
 (let (($x1866 (>= z3_icon_x 0.0)))
 (let (($x1865 (= (+ (- 100.0) home_update_words_hight) 0.0)))
 (let ((?x1861 (+ (+ (- (- home_updates_width) home_updates_x) home_update_words_x) home_update_words_width)))
 (let (($x1863 (or $x1773 (= ?x1861 (- 20.0)))))
 (let ((?x1856 (- (- (+ learn_more_y learn_more_hight) home_updates_y) home_updates_hight)))
 (let (($x1858 (or $x1773 (= ?x1856 (- 20.0)))))
 (let (($x1853 (= (+ (- 50.0) learn_more_hight) 0.0)))
 (let (($x1851 (= (+ (- 100.0) learn_more_width) 0.0)))
 (let (($x1849 (or $x1773 (= (- updates_to_your_homepage_y home_updates_y) 20.0))))
 (let (($x1847 (= (+ (- 50.0) updates_to_your_homepage_hight) 0.0)))
 (let (($x1845 (= (+ (- 200.0) updates_to_your_homepage_width) 0.0)))
 (let ((?x1837 (- (- learn_more_y home_update_words_y) home_update_words_hight)))
 (let (($x1843 (or $x1773 (= ?x1837 20.0))))
 (let ((?x1833 (- (+ (- updates_to_your_homepage_y) home_update_words_y) updates_to_your_homepage_hight)))
 (let (($x1841 (or $x1773 (= ?x1833 20.0))))
 (let (($x1839 (or $x1773 (>= ?x1837 0.0))))
 (let (($x1835 (or $x1773 (>= ?x1833 0.0))))
 (let ((?x1829 (+ (+ (- (- learn_more_y) learn_more_hight) home_updates_y) home_updates_hight)))
 (let (($x1831 (or $x1773 (>= ?x1829 0.0))))
 (let (($x1825 (or $x1773 (>= (- learn_more_y home_updates_y) 0.0))))
 (let ((?x1820 (- (+ (- home_updates_width learn_more_x) home_updates_x) learn_more_width)))
 (let (($x1822 (or $x1773 (>= ?x1820 0.0))))
 (let (($x1817 (or $x1773 (>= (- learn_more_x home_updates_x) 20.0))))
 (let ((?x1812 (- (+ (- home_update_words_y) home_updates_y) home_update_words_hight)))
 (let (($x1815 (or $x1773 (>= (+ ?x1812 home_updates_hight) 0.0))))
 (let (($x1809 (or $x1773 (>= (- home_update_words_y home_updates_y) 0.0))))
 (let ((?x1804 (- (- (+ home_updates_width home_updates_x) home_update_words_x) home_update_words_width)))
 (let (($x1806 (or $x1773 (>= ?x1804 0.0))))
 (let (($x1801 (or $x1773 (>= (+ (- home_updates_x) home_update_words_x) 20.0))))
 (let ((?x1796 (+ (+ (- updates_to_your_homepage_y) home_updates_y) home_updates_hight)))
 (let (($x1799 (or $x1773 (>= (- ?x1796 updates_to_your_homepage_hight) 0.0))))
 (let (($x1793 (or $x1773 (>= (- updates_to_your_homepage_y home_updates_y) 0.0))))
 (let ((?x1787 (- (- home_updates_width updates_to_your_homepage_width) updates_to_your_homepage_x)))
 (let (($x1790 (or $x1773 (>= (+ ?x1787 home_updates_x) 0.0))))
 (let (($x1785 (or $x1773 (>= (- updates_to_your_homepage_x home_updates_x) 20.0))))
 (let (($x1783 (or $x1773 (= (- learn_more_x home_updates_x) 20.0))))
 (let (($x1780 (or $x1773 (= (+ (- home_updates_x) home_update_words_x) 20.0))))
 (let (($x1776 (or $x1773 (= (- updates_to_your_homepage_x home_updates_x) 20.0))))
 (let (($x1772 (>= learn_more_hight 0.0)))
 (let (($x1771 (>= learn_more_width 0.0)))
 (let (($x1770 (>= learn_more_y 0.0)))
 (let (($x1769 (>= learn_more_x 0.0)))
 (let (($x1768 (>= home_update_words_hight 0.0)))
 (let (($x1767 (>= home_update_words_width 0.0)))
 (let (($x1766 (>= home_update_words_y 0.0)))
 (let (($x1765 (>= home_update_words_x 0.0)))
 (let (($x1764 (>= updates_to_your_homepage_hight 0.0)))
 (let (($x1763 (>= updates_to_your_homepage_width 0.0)))
 (let (($x1762 (>= updates_to_your_homepage_y 0.0)))
 (let (($x1761 (>= updates_to_your_homepage_x 0.0)))
 (let (($x1759 (= (- (+ (- (- 10.0) send_feedback_width) filter_x) send_feedback_x) 0.0)))
 (let (($x1760 (or $x1660 $x1759)))
 (let (($x1663 (or $x1660 (= (- home_icon_x home_title_x) 0.0))))
 (let (($x1755 (or $x1660 (= home_icon_width 100.0))))
 (let (($x1753 (or $x1660 (= (- home_icon_width filter_width) 0.0))))
 (let (($x1750 (or $x1660 (= (+ (- send_feedback_width) home_icon_width) 0.0))))
 (let (($x1746 (>= (- (+ (- send_feedback_width) filter_x) send_feedback_x) 0.0)))
 (let (($x1747 (or $x1660 $x1746)))
 (let (($x1741 (>= (+ (- (- home_icon_x) home_icon_width) send_feedback_x) 0.0)))
 (let (($x1742 (or $x1660 $x1741)))
 (let ((?x1735 (+ (- (+ (- filter_y) home_title_y) filter_hight) home_title_hight)))
 (let (($x1737 (or $x1660 (>= ?x1735 0.0))))
 (let (($x1731 (or $x1660 (>= (- filter_y home_title_y) 0.0))))
 (let (($x1728 (>= (- (+ (- home_title_width filter_x) home_title_x) filter_width) 0.0)))
 (let (($x1729 (or $x1660 $x1728)))
 (let (($x1724 (or $x1660 (>= (- filter_x home_title_x) 0.0))))
 (let ((?x1719 (- (+ (- home_title_y send_feedback_y) home_title_hight) send_feedback_hight)))
 (let (($x1721 (or $x1660 (>= ?x1719 0.0))))
 (let (($x1716 (or $x1660 (>= (+ (- home_title_y) send_feedback_y) 0.0))))
 (let ((?x1712 (- (+ (- home_title_width send_feedback_width) home_title_x) send_feedback_x)))
 (let (($x1714 (or $x1660 (>= ?x1712 0.0))))
 (let (($x1709 (or $x1660 (>= (+ (- home_title_x) send_feedback_x) 0.0))))
 (let ((?x1703 (- (+ (+ (- home_icon_hight) home_title_y) home_title_hight) home_icon_y)))
 (let (($x1705 (or $x1660 (>= ?x1703 0.0))))
 (let (($x1699 (or $x1660 (>= (+ (- home_title_y) home_icon_y) 0.0))))
 (let ((?x1695 (+ (- (- home_title_width home_icon_x) home_icon_width) home_title_x)))
 (let (($x1697 (or $x1660 (>= ?x1695 0.0))))
 (let (($x1692 (or $x1660 (>= (- home_icon_x home_title_x) 0.0))))
 (let (($x1689 (= (- (+ (- filter_y home_title_y) filter_hight) home_title_hight) 0.0)))
 (let (($x1690 (or $x1660 $x1689)))
 (let ((?x1684 (+ (- (+ (- home_title_y) send_feedback_y) home_title_hight) send_feedback_hight)))
 (let (($x1686 (or $x1660 (= ?x1684 0.0))))
 (let ((?x1680 (+ (- (- home_icon_hight home_title_y) home_title_hight) home_icon_y)))
 (let (($x1682 (or $x1660 (= ?x1680 0.0))))
 (let (($x1677 (or $x1660 (= (- filter_y home_title_y) 0.0))))
 (let (($x1674 (or $x1660 (= (+ (- home_title_y) send_feedback_y) 0.0))))
 (let (($x1671 (or $x1660 (= (+ (- home_title_y) home_icon_y) 0.0))))
 (let ((?x1666 (+ (- (+ (- home_title_width) filter_x) home_title_x) filter_width)))
 (let (($x1668 (or $x1660 (= ?x1666 0.0))))
 (let (($x1659 (= home_title_hight 50.0)))
 (let (($x1658 (>= filter_hight 0.0)))
 (let (($x1657 (>= filter_width 0.0)))
 (let (($x1656 (>= filter_y 0.0)))
 (let (($x1655 (>= filter_x 0.0)))
 (let (($x1654 (>= send_feedback_hight 0.0)))
 (let (($x1653 (>= send_feedback_width 0.0)))
 (let (($x1652 (>= send_feedback_y 0.0)))
 (let (($x1651 (>= send_feedback_x 0.0)))
 (let (($x1650 (>= home_icon_hight 0.0)))
 (let (($x1649 (>= home_icon_width 0.0)))
 (let (($x1648 (>= home_icon_y 0.0)))
 (let (($x1647 (>= home_icon_x 0.0)))
 (let (($x1646 (or $x1491 (> left_homes_width 500.0))))
 (let (($x1643 (or $x1370 (= (- left_homes_x right_2_collom_x) 0.0))))
 (let (($x1506 (or $x1491 (= (- rec_x left_homes_x) 0.0))))
 (let (($x1503 (or $x1491 (= (+ (- left_homes_x) cvc_page_x) 0.0))))
 (let (($x1500 (or $x1491 (= (+ (- left_homes_x) z3_page_x) 0.0))))
 (let (($x1497 (or $x1491 (= (+ (- left_homes_x) home_updates_x) 0.0))))
 (let (($x1494 (or $x1491 (= (+ (- left_homes_x) home_title_x) 0.0))))
 (let (($x1641 (or $x1491 (>= (+ (- (- cvc_page_y) cvc_page_hight) rec_y) 0.0))))
 (let (($x1639 (or $x1491 (>= (- (- cvc_page_y z3_page_y) z3_page_hight) 0.0))))
 (let (($x1637 (or $x1491 (>= (- (- z3_page_y home_updates_y) home_updates_hight) 0.0))))
 (let ((?x1540 (- (+ (- home_title_y) home_updates_y) home_title_hight)))
 (let (($x1635 (or $x1491 (>= ?x1540 0.0))))
 (let (($x1632 (>= (+ (- (+ (- rec_hight) left_homes_hight) rec_y) left_homes_y) 0.0)))
 (let (($x1633 (or $x1491 $x1632)))
 (let (($x1627 (or $x1491 (>= (- rec_y left_homes_y) 0.0))))
 (let (($x1623 (>= (+ (- (+ (- rec_x) left_homes_x) rec_width) left_homes_width) 0.0)))
 (let (($x1624 (or $x1491 $x1623)))
 (let (($x1618 (or $x1491 (>= (- rec_x left_homes_x) 0.0))))
 (let ((?x1614 (+ (- (+ (- cvc_page_y) left_homes_hight) cvc_page_hight) left_homes_y)))
 (let (($x1616 (or $x1491 (>= ?x1614 0.0))))
 (let (($x1611 (or $x1491 (>= (- cvc_page_y left_homes_y) 0.0))))
 (let ((?x1606 (- (+ (- left_homes_x cvc_page_x) left_homes_width) cvc_page_width)))
 (let (($x1608 (or $x1491 (>= ?x1606 0.0))))
 (let (($x1603 (or $x1491 (>= (+ (- left_homes_x) cvc_page_x) 0.0))))
 (let (($x1600 (>= (+ (- (- left_homes_hight z3_page_y) z3_page_hight) left_homes_y) 0.0)))
 (let (($x1601 (or $x1491 $x1600)))
 (let (($x1596 (or $x1491 (>= (- z3_page_y left_homes_y) 0.0))))
 (let (($x1592 (>= (- (- (+ left_homes_x left_homes_width) z3_page_x) z3_page_width) 0.0)))
 (let (($x1593 (or $x1491 $x1592)))
 (let (($x1588 (or $x1491 (>= (+ (- left_homes_x) z3_page_x) 0.0))))
 (let ((?x1584 (+ (- (- left_homes_hight home_updates_y) home_updates_hight) left_homes_y)))
 (let (($x1586 (or $x1491 (>= ?x1584 0.0))))
 (let (($x1581 (or $x1491 (>= (- home_updates_y left_homes_y) 0.0))))
 (let ((?x1576 (- (+ (+ (- home_updates_width) left_homes_x) left_homes_width) home_updates_x)))
 (let (($x1578 (or $x1491 (>= ?x1576 0.0))))
 (let (($x1572 (or $x1491 (>= (+ (- left_homes_x) home_updates_x) 0.0))))
 (let ((?x1568 (+ (- (- left_homes_hight home_title_y) home_title_hight) left_homes_y)))
 (let (($x1570 (or $x1491 (>= ?x1568 0.0))))
 (let (($x1565 (or $x1491 (>= (- home_title_y left_homes_y) 0.0))))
 (let ((?x1561 (- (+ (+ (- home_title_width) left_homes_x) left_homes_width) home_title_x)))
 (let (($x1563 (or $x1491 (>= ?x1561 0.0))))
 (let (($x1557 (or $x1491 (>= (+ (- left_homes_x) home_title_x) 0.0))))
 (let (($x1555 (or $x1491 (= (+ (- (- cvc_page_y) cvc_page_hight) rec_y) 20.0))))
 (let (($x1550 (or $x1491 (= (- (- cvc_page_y z3_page_y) z3_page_hight) 20.0))))
 (let (($x1546 (or $x1491 (= (- (- z3_page_y home_updates_y) home_updates_hight) 20.0))))
 (let (($x1542 (or $x1491 (= ?x1540 20.0))))
 (let (($x1536 (= (- (+ (- rec_hight left_homes_hight) rec_y) left_homes_y) 0.0)))
 (let (($x1537 (or $x1491 $x1536)))
 (let (($x1532 (or $x1491 (= (- home_title_y left_homes_y) 0.0))))
 (let (($x1528 (= (- (+ (- rec_x left_homes_x) rec_width) left_homes_width) 0.0)))
 (let (($x1529 (or $x1491 $x1528)))
 (let ((?x1523 (+ (- (+ (- left_homes_x) cvc_page_x) left_homes_width) cvc_page_width)))
 (let (($x1525 (or $x1491 (= ?x1523 0.0))))
 (let ((?x1519 (+ (+ (- (- left_homes_x) left_homes_width) z3_page_x) z3_page_width)))
 (let (($x1521 (or $x1491 (= ?x1519 0.0))))
 (let ((?x1514 (+ (- (- home_updates_width left_homes_x) left_homes_width) home_updates_x)))
 (let (($x1516 (or $x1491 (= ?x1514 0.0))))
 (let ((?x1509 (+ (- (- home_title_width left_homes_x) left_homes_width) home_title_x)))
 (let (($x1511 (or $x1491 (= ?x1509 0.0))))
 (let (($x1490 (>= rec_hight 0.0)))
 (let (($x1489 (>= rec_width 0.0)))
 (let (($x1488 (>= rec_y 0.0)))
 (let (($x1487 (>= rec_x 0.0)))
 (let (($x1486 (>= cvc_page_hight 0.0)))
 (let (($x1485 (>= cvc_page_width 0.0)))
 (let (($x1484 (>= cvc_page_y 0.0)))
 (let (($x1483 (>= cvc_page_x 0.0)))
 (let (($x1482 (>= z3_page_hight 0.0)))
 (let (($x1481 (>= z3_page_width 0.0)))
 (let (($x1480 (>= z3_page_y 0.0)))
 (let (($x1479 (>= z3_page_x 0.0)))
 (let (($x1478 (>= home_updates_hight 0.0)))
 (let (($x1477 (>= home_updates_width 0.0)))
 (let (($x1476 (>= home_updates_y 0.0)))
 (let (($x1475 (>= home_updates_x 0.0)))
 (let (($x1474 (>= home_title_hight 0.0)))
 (let (($x1473 (>= home_title_width 0.0)))
 (let (($x1472 (>= home_title_y 0.0)))
 (let (($x1471 (>= home_title_x 0.0)))
 (let (($x1464 (> home_collom_width 1000.0)))
 (let (($x1470 (or $x1464 (= (- home_collom_width right_2_collom_width) 20.0))))
 (let (($x1466 (= right_2_collom_width 1000.0)))
 (let (($x1467 (or (not $x1464) $x1466)))
 (let (($x1462 (or $x1370 (>= (- (- right_homes_x left_homes_x) left_homes_width) 0.0))))
 (let ((?x1458 (- (- (+ right_2_collom_y right_2_collom_hight) right_homes_y) right_homes_hight)))
 (let (($x1460 (or $x1370 (>= ?x1458 0.0))))
 (let (($x1455 (or $x1370 (>= ?x1453 0.0))))
 (let ((?x1450 (+ (+ (- (- right_homes_x) right_homes_width) right_2_collom_x) right_2_collom_width)))
 (let (($x1452 (or $x1370 (>= ?x1450 0.0))))
 (let (($x1446 (or $x1370 (>= (- right_homes_x right_2_collom_x) 0.0))))
 (let ((?x1441 (- (+ (- right_2_collom_y left_homes_hight) right_2_collom_hight) left_homes_y)))
 (let (($x1443 (or $x1370 (>= ?x1441 0.0))))
 (let (($x1438 (or $x1370 (>= (+ ?x1435 left_homes_y) 0.0))))
 (let ((?x1432 (+ (- (+ (- left_homes_x) right_2_collom_x) left_homes_width) right_2_collom_width)))
 (let (($x1434 (or $x1370 (>= ?x1432 0.0))))
 (let (($x1428 (or $x1370 (>= (- left_homes_x right_2_collom_x) 0.0))))
 (let (($x1425 (or $x1370 (= (- (- right_homes_x left_homes_x) left_homes_width) 20.0))))
 (let (($x1421 (>= right_homes_hight 0.0)))
 (let (($x1420 (>= right_homes_width 0.0)))
 (let (($x1419 (>= right_homes_y 0.0)))
 (let (($x1418 (>= right_homes_x 0.0)))
 (let (($x1417 (>= left_homes_hight 0.0)))
 (let (($x1416 (>= left_homes_width 0.0)))
 (let (($x1415 (>= left_homes_y 0.0)))
 (let (($x1414 (>= left_homes_x 0.0)))
 (let (($x1413 (or $x1344 (= (- home_collom_holder_y home_collom_y) 20.0))))
 (let ((?x1408 (* 2.0 home_collom_x)))
 (let ((?x1410 (+ (- (+ (- home_collom_width) (* 2.0 home_collom_holder_x)) ?x1408) home_collom_holder_width)))
 (let (($x1411 (= ?x1410 0.0)))
 (let (($x1404 (or $x1370 $x1385 $x1402)))
 (let (($x1403 (or right_2_collom_feasible right_1_collom_feasible $x1402)))
 (let ((?x1398 (- (+ (- home_collom_holder_y) right_1_collom_hight) home_collom_holder_hight)))
 (let (($x1401 (or $x1385 (= (+ ?x1398 right_1_collom_y) 0.0))))
 (let (($x1396 (or $x1385 (= (+ (- home_collom_holder_y) right_1_collom_y) 0.0))))
 (let ((?x1391 (- (- (+ right_1_collom_x right_1_collom_width) home_collom_holder_x) home_collom_holder_width)))
 (let (($x1393 (or $x1385 (= ?x1391 0.0))))
 (let (($x1388 (or $x1385 (= (- right_1_collom_x home_collom_holder_x) 0.0))))
 (let ((?x1382 (- (+ (- right_2_collom_y home_collom_holder_y) right_2_collom_hight) home_collom_holder_hight)))
 (let (($x1384 (or $x1370 (= ?x1382 0.0))))
 (let (($x1380 (or $x1370 (= (- right_2_collom_y home_collom_holder_y) 0.0))))
 (let ((?x1375 (- (+ (- right_2_collom_x home_collom_holder_x) right_2_collom_width) home_collom_holder_width)))
 (let (($x1377 (or $x1370 (= ?x1375 0.0))))
 (let (($x1373 (or $x1370 (= (- right_2_collom_x home_collom_holder_x) 0.0))))
 (let (($x1369 (>= right_1_collom_hight 0.0)))
 (let (($x1368 (>= right_1_collom_width 0.0)))
 (let (($x1367 (>= right_1_collom_y 0.0)))
 (let (($x1366 (>= right_1_collom_x 0.0)))
 (let (($x1365 (>= right_2_collom_hight 0.0)))
 (let (($x1364 (>= right_2_collom_width 0.0)))
 (let (($x1363 (>= right_2_collom_y 0.0)))
 (let (($x1362 (>= right_2_collom_x 0.0)))
 (let ((?x1358 (- (+ (- home_collom_holder_y) home_collom_y) home_collom_holder_hight)))
 (let (($x1361 (or $x1344 (>= (+ ?x1358 home_collom_hight) 0.0))))
 (let (($x1355 (or $x1344 (>= (- home_collom_holder_y home_collom_y) 0.0))))
 (let ((?x1350 (- (+ (- home_collom_width home_collom_holder_x) home_collom_x) home_collom_holder_width)))
 (let (($x1352 (or $x1344 (>= ?x1350 0.0))))
 (let (($x1347 (or $x1344 (>= (- home_collom_holder_x home_collom_x) 0.0))))
 (let (($x1343 (>= home_collom_holder_hight 0.0)))
 (let (($x1342 (>= home_collom_holder_width 0.0)))
 (let (($x1341 (>= home_collom_holder_y 0.0)))
 (let (($x1340 (>= home_collom_holder_x 0.0)))
 (let (($x1338 (= (- (+ (+ (- side_bar_width) links_width) links_x) side_bar_x) (- 20.0))))
 (let (($x1339 (or $x1122 $x1338)))
 (let (($x1334 (= (+ (- 100.0) links_hight) 0.0)))
 (let (($x1332 (or $x1122 (= recent_act_width 150.0))))
 (let (($x1329 (= (+ (- 50.0) recent_act_hight) 0.0)))
 (let (($x1327 (or $x1122 (= show_more_width 100.0))))
 (let (($x1325 (= (+ (- 50.0) show_more_hight) 0.0)))
 (let (($x1322 (= (- (+ (+ (- side_bar_width) repos_x) repos_width) side_bar_x) (- 20.0))))
 (let (($x1323 (or $x1122 $x1322)))
 (let (($x1318 (= (+ (- 200.0) repos_hight) 0.0)))
 (let ((?x1313 (- (+ (+ (- side_bar_width) find_repo_x) find_repo_width) side_bar_x)))
 (let (($x1315 (or $x1122 (= ?x1313 (- 20.0)))))
 (let (($x1310 (= (+ (- 50.0) find_repo_hight) 0.0)))
 (let ((?x1305 (- (+ (+ (- side_bar_width) top_repo_x) top_repo_width) side_bar_x)))
 (let (($x1308 (or $x1122 (= ?x1305 (- 20.0)))))
 (let (($x1302 (= (+ (- 50.0) top_repo_hight) 0.0)))
 (let (($x1300 (or $x1122 (= user_name_width 100.0))))
 (let (($x1297 (= (+ (- 50.0) user_name_hight) 0.0)))
 (let (($x1295 (or $x1122 (= (- links_x side_bar_x) 20.0))))
 (let (($x1293 (or $x1122 (= (- recent_act_x side_bar_x) 20.0))))
 (let (($x1291 (or $x1122 (= (- show_more_x side_bar_x) 20.0))))
 (let (($x1289 (or $x1122 (= (- repos_x side_bar_x) 20.0))))
 (let (($x1287 (or $x1122 (= (- find_repo_x side_bar_x) 20.0))))
 (let (($x1285 (or $x1122 (= (- top_repo_x side_bar_x) 20.0))))
 (let (($x1283 (or $x1122 (= (- user_name_x side_bar_x) 20.0))))
 (let (($x1281 (or $x988 (= side_bar_width 300.0))))
 (let (($x1278 (or $x1122 (>= (- (+ (- recent_act_y) links_y) recent_act_hight) 0.0))))
 (let (($x1276 (or $x1122 (>= (- (- recent_act_y show_more_y) show_more_hight) 0.0))))
 (let (($x1274 (or $x1122 (>= (- (+ (- repos_hight) show_more_y) repos_y) 0.0))))
 (let (($x1272 (or $x1122 (>= (+ (- (- find_repo_hight) find_repo_y) repos_y) 0.0))))
 (let (($x1270 (or $x1122 (>= (+ (- (- top_repo_y) top_repo_hight) find_repo_y) 0.0))))
 (let (($x1268 (or $x1122 (>= (- (- top_repo_y user_name_y) user_name_hight) 0.0))))
 (let (($x1265 (>= (- (+ (- side_bar_y links_y) side_bar_hight) links_hight) 20.0)))
 (let (($x1266 (or $x1122 $x1265)))
 (let (($x1261 (or $x1122 (>= (+ (- side_bar_y) links_y) 20.0))))
 (let (($x1257 (>= (+ (- (- side_bar_width links_width) links_x) side_bar_x) 20.0)))
 (let (($x1258 (or $x1122 $x1257)))
 (let (($x1253 (or $x1122 (>= (- links_x side_bar_x) 20.0))))
 (let ((?x1248 (+ (- (+ (- recent_act_y) side_bar_y) recent_act_hight) side_bar_hight)))
 (let (($x1250 (or $x1122 (>= ?x1248 20.0))))
 (let (($x1245 (or $x1122 (>= (- recent_act_y side_bar_y) 20.0))))
 (let ((?x1240 (+ (- (+ (- recent_act_width) side_bar_width) recent_act_x) side_bar_x)))
 (let (($x1242 (or $x1122 (>= ?x1240 20.0))))
 (let (($x1236 (or $x1122 (>= (- recent_act_x side_bar_x) 20.0))))
 (let (($x1232 (>= (- (+ (- side_bar_y show_more_y) side_bar_hight) show_more_hight) 20.0)))
 (let (($x1233 (or $x1122 $x1232)))
 (let (($x1228 (or $x1122 (>= (+ (- side_bar_y) show_more_y) 20.0))))
 (let ((?x1223 (+ (- (+ (- show_more_x) side_bar_width) show_more_width) side_bar_x)))
 (let (($x1225 (or $x1122 (>= ?x1223 20.0))))
 (let (($x1219 (or $x1122 (>= (- show_more_x side_bar_x) 20.0))))
 (let (($x1215 (>= (- (+ (+ (- repos_hight) side_bar_y) side_bar_hight) repos_y) 20.0)))
 (let (($x1216 (or $x1122 $x1215)))
 (let (($x1211 (or $x1122 (>= (+ (- side_bar_y) repos_y) 20.0))))
 (let (($x1207 (>= (+ (- (- side_bar_width repos_x) repos_width) side_bar_x) 20.0)))
 (let (($x1208 (or $x1122 $x1207)))
 (let (($x1203 (or $x1122 (>= (- repos_x side_bar_x) 20.0))))
 (let ((?x1198 (- (+ (+ (- find_repo_hight) side_bar_y) side_bar_hight) find_repo_y)))
 (let (($x1200 (or $x1122 (>= ?x1198 20.0))))
 (let (($x1195 (or $x1122 (>= (+ (- side_bar_y) find_repo_y) 20.0))))
 (let (($x1190 (>= (+ (- (- side_bar_width find_repo_x) find_repo_width) side_bar_x) 20.0)))
 (let (($x1191 (or $x1122 $x1190)))
 (let (($x1186 (or $x1122 (>= (- find_repo_x side_bar_x) 20.0))))
 (let ((?x1181 (+ (+ (- (- top_repo_y) top_repo_hight) side_bar_y) side_bar_hight)))
 (let (($x1183 (or $x1122 (>= ?x1181 20.0))))
 (let (($x1179 (or $x1122 (>= (- top_repo_y side_bar_y) 20.0))))
 (let (($x1175 (>= (+ (- (- side_bar_width top_repo_x) top_repo_width) side_bar_x) 20.0)))
 (let (($x1176 (or $x1122 $x1175)))
 (let (($x1171 (or $x1122 (>= (- top_repo_x side_bar_x) 20.0))))
 (let ((?x1166 (+ (- (+ (- user_name_y) side_bar_y) user_name_hight) side_bar_hight)))
 (let (($x1168 (or $x1122 (>= ?x1166 20.0))))
 (let (($x1162 (or $x1122 (>= (- user_name_y side_bar_y) 20.0))))
 (let (($x1158 (>= (- (+ (- side_bar_width user_name_x) side_bar_x) user_name_width) 20.0)))
 (let (($x1159 (or $x1122 $x1158)))
 (let (($x1154 (or $x1122 (>= (- user_name_x side_bar_x) 20.0))))
 (let (($x1151 (or $x1122 (= (- (+ (- recent_act_y) links_y) recent_act_hight) 20.0))))
 (let (($x1146 (or $x1122 (= (- (- recent_act_y show_more_y) show_more_hight) 20.0))))
 (let (($x1142 (or $x1122 (= (- (+ (- repos_hight) show_more_y) repos_y) 20.0))))
 (let (($x1137 (or $x1122 (= (+ (- (- find_repo_hight) find_repo_y) repos_y) 20.0))))
 (let (($x1132 (or $x1122 (= (+ (- (- top_repo_y) top_repo_hight) find_repo_y) 20.0))))
 (let (($x1127 (or $x1122 (= (- (- top_repo_y user_name_y) user_name_hight) 20.0))))
 (let (($x1121 (>= links_hight 0.0)))
 (let (($x1120 (>= links_width 0.0)))
 (let (($x1119 (>= links_y 0.0)))
 (let (($x1118 (>= links_x 0.0)))
 (let (($x1117 (>= recent_act_hight 0.0)))
 (let (($x1116 (>= recent_act_width 0.0)))
 (let (($x1115 (>= recent_act_y 0.0)))
 (let (($x1114 (>= recent_act_x 0.0)))
 (let (($x1113 (>= show_more_hight 0.0)))
 (let (($x1112 (>= show_more_width 0.0)))
 (let (($x1111 (>= show_more_y 0.0)))
 (let (($x1110 (>= show_more_x 0.0)))
 (let (($x1109 (>= repos_hight 0.0)))
 (let (($x1108 (>= repos_width 0.0)))
 (let (($x1107 (>= repos_y 0.0)))
 (let (($x1106 (>= repos_x 0.0)))
 (let (($x1105 (>= find_repo_hight 0.0)))
 (let (($x1104 (>= find_repo_width 0.0)))
 (let (($x1103 (>= find_repo_y 0.0)))
 (let (($x1102 (>= find_repo_x 0.0)))
 (let (($x1101 (>= top_repo_hight 0.0)))
 (let (($x1100 (>= top_repo_width 0.0)))
 (let (($x1099 (>= top_repo_y 0.0)))
 (let (($x1098 (>= top_repo_x 0.0)))
 (let (($x1097 (>= user_name_hight 0.0)))
 (let (($x1096 (>= user_name_width 0.0)))
 (let (($x1095 (>= user_name_y 0.0)))
 (let (($x1094 (>= user_name_x 0.0)))
 (let (($x1093 (or $x988 (= (+ (- (- side_bar_width) side_bar_x) home_collom_x) 0.0))))
 (let ((?x1089 (- (+ (+ (- main_2_collom_hight) home_collom_y) home_collom_hight) main_2_collom_y)))
 (let (($x1091 (or $x988 (= ?x1089 0.0))))
 (let ((?x1084 (- (+ (+ (- main_2_collom_hight) side_bar_y) side_bar_hight) main_2_collom_y)))
 (let (($x1086 (or $x988 (= ?x1084 0.0))))
 (let (($x1080 (or $x988 (= (- home_collom_y main_2_collom_y) 0.0))))
 (let (($x1078 (or $x988 (= (- side_bar_y main_2_collom_y) 0.0))))
 (let ((?x1074 (+ (- (- home_collom_width main_2_collom_x) main_2_collom_width) home_collom_x)))
 (let (($x1076 (or $x988 (= ?x1074 0.0))))
 (let (($x1071 (or $x988 (= (+ (- main_2_collom_x) side_bar_x) 0.0))))
 (let (($x1069 (or $x988 (>= (+ (- (- side_bar_width) side_bar_x) home_collom_x) 0.0))))
 (let ((?x1063 (+ (- (- main_2_collom_hight home_collom_y) home_collom_hight) main_2_collom_y)))
 (let (($x1065 (or $x988 (>= ?x1063 0.0))))
 (let (($x1060 (or $x988 (>= (- home_collom_y main_2_collom_y) 0.0))))
 (let ((?x1055 (- (+ (+ (- home_collom_width) main_2_collom_x) main_2_collom_width) home_collom_x)))
 (let (($x1057 (or $x988 (>= ?x1055 0.0))))
 (let (($x1051 (or $x988 (>= (+ (- main_2_collom_x) home_collom_x) 0.0))))
 (let ((?x1046 (+ (- (- main_2_collom_hight side_bar_y) side_bar_hight) main_2_collom_y)))
 (let (($x1048 (or $x988 (>= ?x1046 0.0))))
 (let (($x1043 (or $x988 (>= (- side_bar_y main_2_collom_y) 0.0))))
 (let ((?x1038 (- (+ (+ (- side_bar_width) main_2_collom_x) main_2_collom_width) side_bar_x)))
 (let (($x1040 (or $x988 (>= ?x1038 0.0))))
 (let (($x1034 (or $x988 (>= (+ (- main_2_collom_x) side_bar_x) 0.0))))
 (let (($x1030 (>= home_collom_hight 0.0)))
 (let (($x1029 (>= home_collom_width 0.0)))
 (let (($x1028 (>= home_collom_y 0.0)))
 (let (($x1027 (>= home_collom_x 0.0)))
 (let (($x1026 (>= side_bar_hight 0.0)))
 (let (($x1025 (>= side_bar_width 0.0)))
 (let (($x1024 (>= side_bar_y 0.0)))
 (let (($x1023 (>= side_bar_x 0.0)))
 (let (($x1022 (or $x988 $x1004)))
 (let (($x1021 (or main_2_collom_feasible main_1_collom_feasible)))
 (let ((?x1018 (+ (+ (- (- main_holder_y) main_holder_hight) main_1_collom_y) main_1_collom_hight)))
 (let (($x1020 (or $x1004 (= ?x1018 0.0))))
 (let (($x1015 (or $x1004 (= (+ (- main_holder_y) main_1_collom_y) 0.0))))
 (let ((?x1010 (- (- (+ main_1_collom_x main_1_collom_width) main_holder_x) main_holder_width)))
 (let (($x1012 (or $x1004 (= ?x1010 0.0))))
 (let (($x1007 (or $x1004 (= (- main_1_collom_x main_holder_x) 0.0))))
 (let ((?x1001 (+ (- (- main_2_collom_hight main_holder_y) main_holder_hight) main_2_collom_y)))
 (let (($x1003 (or $x988 (= ?x1001 0.0))))
 (let (($x998 (or $x988 (= (+ (- main_holder_y) main_2_collom_y) 0.0))))
 (let ((?x993 (- (+ (- main_2_collom_x main_holder_x) main_2_collom_width) main_holder_width)))
 (let (($x995 (or $x988 (= ?x993 0.0))))
 (let (($x991 (or $x988 (= (- main_2_collom_x main_holder_x) 0.0))))
 (let (($x987 (>= main_1_collom_hight 0.0)))
 (let (($x986 (>= main_1_collom_width 0.0)))
 (let (($x985 (>= main_1_collom_y 0.0)))
 (let (($x984 (>= main_1_collom_x 0.0)))
 (let (($x983 (>= main_2_collom_hight 0.0)))
 (let (($x982 (>= main_2_collom_width 0.0)))
 (let (($x981 (>= main_2_collom_y 0.0)))
 (let (($x980 (>= main_2_collom_x 0.0)))
 (let ((?x860 (- (- person_x mail_x) mail_width)))
 (let (($x861 (>= ?x860 0.0)))
 (let (($x979 (or $x722 $x861)))
 (let (($x977 (>= (- (+ (+ (- person_hight) mails_2_y) mails_2_hight) person_y) 0.0)))
 (let (($x978 (or $x722 $x977)))
 (let (($x972 (or $x722 (>= (+ (- mails_2_y) person_y) 0.0))))
 (let (($x969 (>= (- (- (+ mails_2_x mails_2_width) person_x) person_width) 0.0)))
 (let (($x970 (or $x722 $x969)))
 (let (($x966 (or $x722 (>= (+ (- mails_2_x) person_x) 0.0))))
 (let (($x962 (>= (+ (+ (- (- mail_y) mail_hight) mails_2_y) mails_2_hight) 0.0)))
 (let (($x963 (or $x722 $x962)))
 (let (($x957 (or $x722 (>= (- mail_y mails_2_y) 0.0))))
 (let (($x954 (>= (- (- (+ mails_2_x mails_2_width) mail_x) mail_width) 0.0)))
 (let (($x955 (or $x722 $x954)))
 (let (($x951 (or $x722 (>= (+ (- mails_2_x) mail_x) 0.0))))
 (let (($x911 (= ?x860 10.0)))
 (let (($x949 (or $x722 $x911)))
 (let (($x947 (= (+ (- (- person_hight mails_2_y) mails_2_hight) person_y) 0.0)))
 (let (($x948 (or $x722 $x947)))
 (let (($x942 (= (- (- (+ mail_y mail_hight) mails_2_y) mails_2_hight) 0.0)))
 (let (($x943 (or $x722 $x942)))
 (let (($x938 (or $x722 (= (+ (- mails_2_y) person_y) 0.0))))
 (let (($x934 (or $x722 (= (- mail_y mails_2_y) 0.0))))
 (let (($x930 (= (+ (+ (- (- mails_2_x) mails_2_width) person_x) person_width) 0.0)))
 (let (($x931 (or $x722 $x930)))
 (let (($x926 (or $x722 (= (+ (- mails_2_x) mail_x) 0.0))))
 (let (($x922 (= (+ (- 100.0) person_width) 0.0)))
 (let (($x920 (= (+ (- 50.0) mail_width) 0.0)))
 (let (($x918 (= (+ (- 50.0) pull_width) 0.0)))
 (let (($x916 (= (+ (- 50.0) point_width) 0.0)))
 (let (($x914 (= (+ (- 100.0) add_width) 0.0)))
 (let (($x912 (or $x704 $x911)))
 (let (($x910 (or $x704 (= (- (- mail_x pull_x) pull_width) 10.0))))
 (let (($x908 (or $x704 (= (- (+ (- point_width) pull_x) point_x) 10.0))))
 (let (($x906 (or $x704 (= (+ (- (- add_width) add_x) point_x) 10.0))))
 (let (($x903 (= (+ (- (+ (- mails_1_hight) person_hight) mails_1_y) person_y) 0.0)))
 (let (($x904 (or $x704 $x903)))
 (let (($x898 (= (- (+ (+ (- mails_1_hight) mail_y) mail_hight) mails_1_y) 0.0)))
 (let (($x899 (or $x704 $x898)))
 (let (($x893 (= (- (+ (+ (- mails_1_hight) pull_y) pull_hight) mails_1_y) 0.0)))
 (let (($x894 (or $x704 $x893)))
 (let (($x888 (= (- (+ (+ (- mails_1_hight) point_y) point_hight) mails_1_y) 0.0)))
 (let (($x889 (or $x704 $x888)))
 (let (($x883 (= (- (+ (+ (- mails_1_hight) add_y) add_hight) mails_1_y) 0.0)))
 (let (($x884 (or $x704 $x883)))
 (let (($x878 (or $x704 (= (+ (- mails_1_y) person_y) 0.0))))
 (let (($x876 (or $x704 (= (- mail_y mails_1_y) 0.0))))
 (let (($x874 (or $x704 (= (- pull_y mails_1_y) 0.0))))
 (let (($x872 (or $x704 (= (- point_y mails_1_y) 0.0))))
 (let (($x870 (or $x704 (= (- add_y mails_1_y) 0.0))))
 (let (($x867 (= (+ (- (+ (- mails_1_x) person_x) mails_1_width) person_width) 0.0)))
 (let (($x868 (or $x704 $x867)))
 (let (($x864 (or $x704 (= (+ (- mails_1_x) add_x) 0.0))))
 (let (($x862 (or $x704 $x861)))
 (let (($x858 (or $x704 (>= (- (- mail_x pull_x) pull_width) 0.0))))
 (let (($x854 (or $x704 (>= (- (+ (- point_width) pull_x) point_x) 0.0))))
 (let (($x850 (or $x704 (>= (+ (- (- add_width) add_x) point_x) 0.0))))
 (let (($x845 (>= (- (+ (- mails_1_hight person_hight) mails_1_y) person_y) 0.0)))
 (let (($x846 (or $x704 $x845)))
 (let (($x841 (or $x704 (>= (+ (- mails_1_y) person_y) 0.0))))
 (let (($x836 (>= (- (+ (- mails_1_x person_x) mails_1_width) person_width) 0.0)))
 (let (($x837 (or $x704 $x836)))
 (let (($x832 (or $x704 (>= (+ (- mails_1_x) person_x) 0.0))))
 (let (($x828 (>= (+ (- (- mails_1_hight mail_y) mail_hight) mails_1_y) 0.0)))
 (let (($x829 (or $x704 $x828)))
 (let (($x824 (or $x704 (>= (- mail_y mails_1_y) 0.0))))
 (let (($x820 (>= (- (- (+ mails_1_x mails_1_width) mail_x) mail_width) 0.0)))
 (let (($x821 (or $x704 $x820)))
 (let (($x817 (or $x704 (>= (+ (- mails_1_x) mail_x) 0.0))))
 (let (($x813 (>= (+ (- (- mails_1_hight pull_y) pull_hight) mails_1_y) 0.0)))
 (let (($x814 (or $x704 $x813)))
 (let (($x809 (or $x704 (>= (- pull_y mails_1_y) 0.0))))
 (let (($x805 (>= (- (- (+ mails_1_x mails_1_width) pull_x) pull_width) 0.0)))
 (let (($x806 (or $x704 $x805)))
 (let (($x802 (or $x704 (>= (+ (- mails_1_x) pull_x) 0.0))))
 (let (($x798 (>= (+ (- (- mails_1_hight point_y) point_hight) mails_1_y) 0.0)))
 (let (($x799 (or $x704 $x798)))
 (let (($x794 (or $x704 (>= (- point_y mails_1_y) 0.0))))
 (let (($x790 (>= (- (+ (+ (- point_width) mails_1_x) mails_1_width) point_x) 0.0)))
 (let (($x791 (or $x704 $x790)))
 (let (($x785 (or $x704 (>= (+ (- mails_1_x) point_x) 0.0))))
 (let (($x782 (or $x704 (>= (+ (- (- mails_1_hight add_y) add_hight) mails_1_y) 0.0))))
 (let (($x777 (or $x704 (>= (- add_y mails_1_y) 0.0))))
 (let (($x773 (>= (- (+ (+ (- add_width) mails_1_x) mails_1_width) add_x) 0.0)))
 (let (($x774 (or $x704 $x773)))
 (let (($x768 (or $x704 (>= (+ (- mails_1_x) add_x) 0.0))))
 (let (($x764 (>= person_hight 0.0)))
 (let (($x763 (>= person_width 0.0)))
 (let (($x762 (>= person_y 0.0)))
 (let (($x761 (>= person_x 0.0)))
 (let (($x760 (>= mail_hight 0.0)))
 (let (($x759 (>= mail_width 0.0)))
 (let (($x758 (>= mail_y 0.0)))
 (let (($x757 (>= mail_x 0.0)))
 (let (($x756 (>= pull_hight 0.0)))
 (let (($x755 (>= pull_width 0.0)))
 (let (($x754 (>= pull_y 0.0)))
 (let (($x753 (>= pull_x 0.0)))
 (let (($x752 (>= point_hight 0.0)))
 (let (($x751 (>= point_width 0.0)))
 (let (($x750 (>= point_y 0.0)))
 (let (($x749 (>= point_x 0.0)))
 (let (($x748 (>= add_hight 0.0)))
 (let (($x747 (>= add_width 0.0)))
 (let (($x746 (>= add_y 0.0)))
 (let (($x745 (>= add_x 0.0)))
 (let ((?x743 (- (+ (- (- 10.0) search_holder_width) mails_holder_x) search_holder_x)))
 (let (($x744 (= ?x743 0.0)))
 (let (($x740 (or $x704 $x722)))
 (let (($x739 (or mails_1_feasible mails_2_feasible)))
 (let ((?x736 (+ (+ (- (- mails_holder_y) mails_holder_hight) mails_2_y) mails_2_hight)))
 (let (($x738 (or $x722 (= ?x736 0.0))))
 (let (($x733 (or $x722 (= (+ (- mails_holder_y) mails_2_y) 0.0))))
 (let ((?x728 (- (- (+ mails_2_x mails_2_width) mails_holder_x) mails_holder_width)))
 (let (($x730 (or $x722 (= ?x728 0.0))))
 (let (($x725 (or $x722 (= (- mails_2_x mails_holder_x) 0.0))))
 (let ((?x719 (+ (- (- mails_1_hight mails_holder_y) mails_holder_hight) mails_1_y)))
 (let (($x721 (or $x704 (= ?x719 0.0))))
 (let (($x716 (or $x704 (= (+ (- mails_holder_y) mails_1_y) 0.0))))
 (let ((?x710 (- (- (+ mails_1_x mails_1_width) mails_holder_x) mails_holder_width)))
 (let (($x712 (or $x704 (= ?x710 0.0))))
 (let (($x707 (or $x704 (= (- mails_1_x mails_holder_x) 0.0))))
 (let (($x703 (>= mails_2_hight 0.0)))
 (let (($x702 (>= mails_2_width 0.0)))
 (let (($x701 (>= mails_2_y 0.0)))
 (let (($x700 (>= mails_2_x 0.0)))
 (let (($x699 (>= mails_1_hight 0.0)))
 (let (($x698 (>= mails_1_width 0.0)))
 (let (($x697 (>= mails_1_y 0.0)))
 (let (($x696 (>= mails_1_x 0.0)))
 (let ((?x592 (+ (- (- dashbord_width) dashbord_x) search_holder_x)))
 (let (($x695 (>= ?x592 200.0)))
 (let (($x693 (= (+ (- 50.0) search_bar_2_width) 0.0)))
 (let (($x690 (= (+ (- 300.0) search_bar_1_width) 0.0)))
 (let (($x668 (not search_bar_2_feasible)))
 (let (($x651 (not search_bar_1_feasible)))
 (let (($x687 (or $x651 $x668)))
 (let (($x686 (or search_bar_1_feasible search_bar_2_feasible)))
 (let ((?x683 (+ (- (- search_bar_2_hight search_holder_y) search_holder_hight) search_bar_2_y)))
 (let (($x685 (or $x668 (= ?x683 0.0))))
 (let (($x680 (or $x668 (= (+ (- search_holder_y) search_bar_2_y) 0.0))))
 (let ((?x674 (- (+ (+ (- search_holder_width) search_bar_2_x) search_bar_2_width) search_holder_x)))
 (let (($x676 (or $x668 (= ?x674 0.0))))
 (let (($x671 (or $x668 (= (- search_bar_2_x search_holder_x) 0.0))))
 (let ((?x665 (- (- (+ search_bar_1_y search_bar_1_hight) search_holder_y) search_holder_hight)))
 (let (($x667 (or $x651 (= ?x665 0.0))))
 (let (($x662 (or $x651 (= (- search_bar_1_y search_holder_y) 0.0))))
 (let ((?x657 (- (+ (+ (- search_holder_width) search_bar_1_x) search_bar_1_width) search_holder_x)))
 (let (($x659 (or $x651 (= ?x657 0.0))))
 (let (($x654 (or $x651 (= (- search_bar_1_x search_holder_x) 0.0))))
 (let (($x650 (>= search_bar_2_hight 0.0)))
 (let (($x649 (>= search_bar_2_width 0.0)))
 (let (($x648 (>= search_bar_2_y 0.0)))
 (let (($x647 (>= search_bar_2_x 0.0)))
 (let (($x646 (>= search_bar_1_hight 0.0)))
 (let (($x645 (>= search_bar_1_width 0.0)))
 (let (($x644 (>= search_bar_1_y 0.0)))
 (let (($x643 (>= search_bar_1_x 0.0)))
 (let (($x642 (= (+ (- 100.0) dashbord_width) 0.0)))
 (let (($x639 (= (+ (- (- (- 10.0) github_icon_x) github_icon_width) dashbord_x) 0.0)))
 (let (($x635 (= (+ (- 30.0) github_icon_width) 0.0)))
 (let (($x633 (= (- (- (+ (- 10.0) github_icon_x) less_icon_x) less_icon_width) 0.0)))
 (let (($x629 (= (+ (- 30.0) less_icon_width) 0.0)))
 (let ((?x625 (+ (- (+ (- title_y) mails_holder_y) title_hight) mails_holder_hight)))
 (let (($x626 (= ?x625 (- 10.0))))
 (let ((?x622 (+ (+ (- (- title_y) title_hight) search_holder_y) search_holder_hight)))
 (let (($x623 (= ?x622 (- 10.0))))
 (let (($x620 (= (+ (+ (- (- title_y) title_hight) dashbord_y) dashbord_hight) (- 10.0))))
 (let (($x616 (= (+ (- (- github_icon_hight title_y) title_hight) github_icon_y) (- 10.0))))
 (let (($x612 (= (- (+ (- less_icon_y title_y) less_icon_hight) title_hight) (- 10.0))))
 (let ((?x454 (- title_y)))
 (let ((?x580 (+ ?x454 mails_holder_y)))
 (let (($x609 (= ?x580 10.0)))
 (let ((?x569 (+ ?x454 search_holder_y)))
 (let (($x608 (= ?x569 10.0)))
 (let ((?x556 (+ ?x454 dashbord_y)))
 (let (($x607 (= ?x556 10.0)))
 (let ((?x541 (+ ?x454 github_icon_y)))
 (let (($x606 (= ?x541 10.0)))
 (let ((?x527 (- less_icon_y title_y)))
 (let (($x605 (= ?x527 10.0)))
 (let ((?x602 (+ (- (+ (- title_x) mails_holder_x) title_width) mails_holder_width)))
 (let (($x604 (= ?x602 (- 10.0))))
 (let ((?x520 (- less_icon_x title_x)))
 (let (($x600 (= ?x520 10.0)))
 (let (($x598 (= title_hight 50.0)))
 (let (($x596 (>= (- (+ (- search_holder_width) mails_holder_x) search_holder_x) 0.0)))
 (let (($x593 (>= ?x592 0.0)))
 (let (($x590 (>= (+ (- (- github_icon_x) github_icon_width) dashbord_x) 0.0)))
 (let (($x588 (>= (- (- github_icon_x less_icon_x) less_icon_width) 0.0)))
 (let (($x585 (>= (- (+ (- title_y mails_holder_y) title_hight) mails_holder_hight) 0.0)))
 (let (($x581 (>= ?x580 0.0)))
 (let (($x579 (>= (- (+ (- title_x mails_holder_x) title_width) mails_holder_width) 0.0)))
 (let ((?x548 (- title_x)))
 (let ((?x574 (+ ?x548 mails_holder_x)))
 (let (($x575 (>= ?x574 0.0)))
 (let ((?x572 (- (- (+ title_y title_hight) search_holder_y) search_holder_hight)))
 (let (($x573 (>= ?x572 0.0)))
 (let (($x570 (>= ?x569 0.0)))
 (let ((?x567 (- (+ (+ (- search_holder_width) title_x) title_width) search_holder_x)))
 (let (($x568 (>= ?x567 0.0)))
 (let (($x563 (>= (+ ?x548 search_holder_x) 0.0)))
 (let (($x561 (>= (- (- (+ title_y title_hight) dashbord_y) dashbord_hight) 0.0)))
 (let (($x557 (>= ?x556 0.0)))
 (let (($x555 (>= (- (+ (+ (- dashbord_width) title_x) title_width) dashbord_x) 0.0)))
 (let (($x550 (>= (+ ?x548 dashbord_x) 0.0)))
 (let ((?x546 (- (+ (+ (- github_icon_hight) title_y) title_hight) github_icon_y)))
 (let (($x547 (>= ?x546 0.0)))
 (let (($x542 (>= ?x541 0.0)))
 (let ((?x539 (+ (+ (- (- github_icon_x) github_icon_width) title_x) title_width)))
 (let (($x540 (>= ?x539 0.0)))
 (let (($x535 (>= (- github_icon_x title_x) 0.0)))
 (let (($x533 (>= (+ (- (+ (- less_icon_y) title_y) less_icon_hight) title_hight) 0.0)))
 (let (($x528 (>= ?x527 0.0)))
 (let (($x526 (>= (+ (- (+ (- less_icon_x) title_x) less_icon_width) title_width) 0.0)))
 (let (($x521 (>= ?x520 0.0)))
 (let (($x519 (>= mails_holder_hight 0.0)))
 (let (($x518 (>= mails_holder_width 0.0)))
 (let (($x517 (>= mails_holder_y 0.0)))
 (let (($x516 (>= mails_holder_x 0.0)))
 (let (($x515 (>= search_holder_hight 0.0)))
 (let (($x514 (>= search_holder_width 0.0)))
 (let (($x513 (>= search_holder_y 0.0)))
 (let (($x512 (>= search_holder_x 0.0)))
 (let (($x511 (>= dashbord_hight 0.0)))
 (let (($x510 (>= dashbord_width 0.0)))
 (let (($x509 (>= dashbord_y 0.0)))
 (let (($x508 (>= dashbord_x 0.0)))
 (let (($x507 (>= github_icon_hight 0.0)))
 (let (($x506 (>= github_icon_width 0.0)))
 (let (($x505 (>= github_icon_y 0.0)))
 (let (($x504 (>= github_icon_x 0.0)))
 (let (($x503 (>= less_icon_hight 0.0)))
 (let (($x502 (>= less_icon_width 0.0)))
 (let (($x501 (>= less_icon_y 0.0)))
 (let (($x500 (>= less_icon_x 0.0)))
 (let (($x499 (= (- back_ground_y BC_y) 0.0)))
 (let (($x497 (= (+ (- (+ (- BC_x) back_ground_width) BC_width) back_ground_x) 0.0)))
 (let (($x493 (= (+ (- BC_x) back_ground_x) 0.0)))
 (let ((?x473 (- (+ ?x454 main_holder_y) title_hight)))
 (let (($x490 (= ?x473 0.0)))
 (let ((?x488 (- (+ (- main_holder_y back_ground_y) main_holder_hight) back_ground_hight)))
 (let (($x489 (= ?x488 0.0)))
 (let ((?x452 (- title_y back_ground_y)))
 (let (($x486 (= ?x452 0.0)))
 (let ((?x484 (+ (- (+ (- back_ground_width) main_holder_x) back_ground_x) main_holder_width)))
 (let (($x485 (= ?x484 0.0)))
 (let ((?x480 (+ (- (+ (- back_ground_width) title_x) back_ground_x) title_width)))
 (let (($x481 (= ?x480 0.0)))
 (let ((?x459 (- main_holder_x back_ground_x)))
 (let (($x476 (= ?x459 0.0)))
 (let ((?x446 (- title_x back_ground_x)))
 (let (($x475 (= ?x446 0.0)))
 (let (($x474 (>= ?x473 0.0)))
 (let ((?x470 (+ (- (+ (- main_holder_y) back_ground_y) main_holder_hight) back_ground_hight)))
 (let (($x471 (>= ?x470 0.0)))
 (let ((?x465 (- main_holder_y back_ground_y)))
 (let (($x466 (>= ?x465 0.0)))
 (let ((?x463 (- (+ (- back_ground_width main_holder_x) back_ground_x) main_holder_width)))
 (let (($x464 (>= ?x463 0.0)))
 (let (($x460 (>= ?x459 0.0)))
 (let (($x458 (>= (+ (- (+ ?x454 back_ground_y) title_hight) back_ground_hight) 0.0)))
 (let (($x453 (>= ?x452 0.0)))
 (let (($x451 (>= (- (+ (- back_ground_width title_x) back_ground_x) title_width) 0.0)))
 (let (($x447 (>= ?x446 0.0)))
 (let (($x445 (>= main_holder_hight 0.0)))
 (let (($x444 (>= main_holder_width 0.0)))
 (let (($x443 (>= main_holder_y 0.0)))
 (let (($x442 (>= main_holder_x 0.0)))
 (let (($x441 (>= title_hight 0.0)))
 (let (($x440 (>= title_width 0.0)))
 (let (($x439 (>= title_y 0.0)))
 (let (($x438 (>= title_x 0.0)))
 (let (($x437 (>= back_ground_hight 0.0)))
 (let (($x436 (>= back_ground_width 0.0)))
 (let (($x435 (>= back_ground_y 0.0)))
 (let (($x434 (>= back_ground_x 0.0)))
 (let (($x433 (= BC_y 0.0)))
 (let (($x432 (= BC_x 0.0)))
 (let (($x431 (<= BC_width 4000.0)))
 (let (($x429 (>= BC_hight 0.0)))
 (let (($x428 (>= BC_width 0.0)))
 (let (($x427 (>= BC_y 0.0)))
 (let (($x426 (>= BC_x 0.0)))
 (and $x426 $x427 $x428 $x429 $x431 $x432 $x433 BC_feasible $x434 $x435 $x436 $x437 $x438 $x439 $x440 $x441 $x442 $x443 $x444 $x445 $x447 $x451 $x453 $x458 $x460 $x464 $x466 $x471 $x474 $x475 $x476 $x481 $x485 $x486 $x489 $x490 $x493 $x497 $x499 $x500 $x501 $x502 $x503 $x504 $x505 $x506 $x507 $x508 $x509 $x510 $x511 $x512 $x513 $x514 $x515 $x516 $x517 $x518 $x519 $x521 $x526 $x528 $x533 $x535 $x540 $x542 $x547 $x550 $x555 $x557 $x561 $x563 $x568 $x570 $x573 $x575 $x579 $x581 $x585 $x588 $x590 $x593 $x596 $x598 $x600 $x604 $x605 $x606 $x607 $x608 $x609 $x612 $x616 $x620 $x623 $x626 $x629 $x633 $x635 $x639 $x642 $x643 $x644 $x645 $x646 $x647 $x648 $x649 $x650 $x654 $x659 $x662 $x667 $x671 $x676 $x680 $x685 $x686 $x687 $x690 $x693 $x695 $x696 $x697 $x698 $x699 $x700 $x701 $x702 $x703 $x707 $x712 $x716 $x721 $x725 $x730 $x733 $x738 $x739 $x740 $x744 $x745 $x746 $x747 $x748 $x749 $x750 $x751 $x752 $x753 $x754 $x755 $x756 $x757 $x758 $x759 $x760 $x761 $x762 $x763 $x764 $x768 $x774 $x777 $x782 $x785 $x791 $x794 $x799 $x802 $x806 $x809 $x814 $x817 $x821 $x824 $x829 $x832 $x837 $x841 $x846 $x850 $x854 $x858 $x862 $x864 $x868 $x870 $x872 $x874 $x876 $x878 $x884 $x889 $x894 $x899 $x904 $x906 $x908 $x910 $x912 $x914 $x916 $x918 $x920 $x922 $x926 $x931 $x934 $x938 $x943 $x948 $x949 $x951 $x955 $x957 $x963 $x966 $x970 $x972 $x978 $x979 $x980 $x981 $x982 $x983 $x984 $x985 $x986 $x987 $x991 $x995 $x998 $x1003 $x1007 $x1012 $x1015 $x1020 $x1021 $x1022 $x1023 $x1024 $x1025 $x1026 $x1027 $x1028 $x1029 $x1030 $x1034 $x1040 $x1043 $x1048 $x1051 $x1057 $x1060 $x1065 $x1069 $x1071 $x1076 $x1078 $x1080 $x1086 $x1091 $x1093 $x1094 $x1095 $x1096 $x1097 $x1098 $x1099 $x1100 $x1101 $x1102 $x1103 $x1104 $x1105 $x1106 $x1107 $x1108 $x1109 $x1110 $x1111 $x1112 $x1113 $x1114 $x1115 $x1116 $x1117 $x1118 $x1119 $x1120 $x1121 $x1127 $x1132 $x1137 $x1142 $x1146 $x1151 $x1154 $x1159 $x1162 $x1168 $x1171 $x1176 $x1179 $x1183 $x1186 $x1191 $x1195 $x1200 $x1203 $x1208 $x1211 $x1216 $x1219 $x1225 $x1228 $x1233 $x1236 $x1242 $x1245 $x1250 $x1253 $x1258 $x1261 $x1266 $x1268 $x1270 $x1272 $x1274 $x1276 $x1278 $x1281 $x1283 $x1285 $x1287 $x1289 $x1291 $x1293 $x1295 $x1297 $x1300 $x1302 $x1308 $x1310 $x1315 $x1318 $x1323 $x1325 $x1327 $x1329 $x1332 $x1334 $x1339 $x1340 $x1341 $x1342 $x1343 $x1347 $x1352 $x1355 $x1361 $x1362 $x1363 $x1364 $x1365 $x1366 $x1367 $x1368 $x1369 $x1373 $x1377 $x1380 $x1384 $x1388 $x1393 $x1396 $x1401 $x1403 $x1404 $x1411 $x1413 $x1414 $x1415 $x1416 $x1417 $x1418 $x1419 $x1420 $x1421 $x1425 $x1428 $x1434 $x1438 $x1443 $x1446 $x1452 $x1455 $x1460 $x1462 $x1467 $x1470 $x1471 $x1472 $x1473 $x1474 $x1475 $x1476 $x1477 $x1478 $x1479 $x1480 $x1481 $x1482 $x1483 $x1484 $x1485 $x1486 $x1487 $x1488 $x1489 $x1490 $x1494 $x1497 $x1500 $x1503 $x1506 $x1511 $x1516 $x1521 $x1525 $x1529 $x1532 $x1537 $x1542 $x1546 $x1550 $x1555 $x1557 $x1563 $x1565 $x1570 $x1572 $x1578 $x1581 $x1586 $x1588 $x1593 $x1596 $x1601 $x1603 $x1608 $x1611 $x1616 $x1618 $x1624 $x1627 $x1633 $x1635 $x1637 $x1639 $x1641 $x1494 $x1497 $x1500 $x1503 $x1506 $x1643 $x1646 $x1647 $x1648 $x1649 $x1650 $x1651 $x1652 $x1653 $x1654 $x1655 $x1656 $x1657 $x1658 $x1659 $x1663 $x1668 $x1671 $x1674 $x1677 $x1682 $x1686 $x1690 $x1692 $x1697 $x1699 $x1705 $x1709 $x1714 $x1716 $x1721 $x1724 $x1729 $x1731 $x1737 $x1742 $x1747 $x1750 $x1753 $x1755 $x1663 $x1760 $x1761 $x1762 $x1763 $x1764 $x1765 $x1766 $x1767 $x1768 $x1769 $x1770 $x1771 $x1772 $x1776 $x1780 $x1783 $x1785 $x1790 $x1793 $x1799 $x1801 $x1806 $x1809 $x1815 $x1817 $x1822 $x1825 $x1831 $x1835 $x1839 $x1841 $x1843 $x1845 $x1847 $x1849 $x1851 $x1853 $x1858 $x1863 $x1865 $x1866 $x1867 $x1868 $x1869 $x1870 $x1871 $x1872 $x1873 $x1874 $x1875 $x1876 $x1877 $x1878 $x1879 $x1880 $x1881 $x1887 $x1892 $x1896 $x1899 $x1905 $x1909 $x1914 $x1917 $x1923 $x1926 $x1931 $x1935 $x1941 $x1944 $x1949 $x1952 $x1957 $x1960 $x1965 $x1967 $x1969 $x1971 $x1973 $x1975 $x1977 $x1979 $x1982 $x1984 $x1986 $x1988 $x1990 $x1995 $x1999 $x2001 $x2003 $x2004 $x2005 $x2006 $x2007 $x2008 $x2009 $x2010 $x2011 $x2012 $x2013 $x2014 $x2015 $x2016 $x2017 $x2018 $x2019 $x2025 $x2030 $x2035 $x2039 $x2045 $x2048 $x2053 $x2056 $x2061 $x2064 $x2069 $x2072 $x2078 $x2081 $x2086 $x2089 $x2095 $x2098 $x2103 $x2105 $x2107 $x2109 $x2111 $x2113 $x2115 $x2117 $x2119 $x2121 $x2123 $x2125 $x2127 $x2131 $x2135 $x2137 $x2139 $x2140 $x2141 $x2142 $x2143 $x2147 $x2150 $x2152 $x2154 $x2155 $x2156 $x2157 $x2158 $x2160 $x2162 $x2165 $x2170 $x2171 $x2172 $x2173 $x2174 $x2179 $x2182 $x2185 $x2187 $x2188 $x2189 $x2190 $x2191 $x2194 $x2198 $x2200 $x2205 $x2206 $x2207 $x2208 $x2209 $x2212 $x2217 $x2219 $x2221 $x2222 $x2223 $x2224 $x2225 $x2230 $x2234 $x2236 $x2238 $x2243 $x2244 $x2245 $x2246 $x2247 $x2248 $x2249 $x2250 $x2251 $x2252 $x2253 $x2254 $x2255 $x2259 $x2262 $x2265 $x2269 $x2273 $x2278 $x2282 $x2287 $x2289 $x2294 $x2296 $x2301 $x2303 $x2308 $x2311 $x2316 $x2318 $x2323 $x2325 $x2331 $x2336 $x2340 $x2342 $x2344 $x2347 $x2350 $x2351 $x2352 $x2353 $x2354 $x2355 $x2356 $x2357 $x2358 $x2359 $x2360 $x2361 $x2362 $x2363 $x2368 $x2373 $x2376 $x2382 $x2385 $x2389 $x2392 $x2398 $x2401 $x2405 $x2408 $x2414 $x2418 $x2422 $x2424 $x2426 $x2428 $x2430 $x2432 $x2437 $x2441 $x2445 $x2447 $x2452 $x2455 $x2459 $x2461 $x2462 $x2463 $x2464 $x2465 $x2466 $x2467 $x2468 $x2469 $x2473 $x2479 $x2483 $x2489 $x2492 $x2498 $x2501 $x2507 $x2511 $x2513 $x2515 $x2520 $x2525 $x2527 $x2531 $x2533 $x2535 $x2536 $x2537 $x2538 $x2539 $x2540 $x2541 $x2542 $x2543 $x2544 $x2545 $x2546 $x2547 $x2548 $x2549 $x2550 $x2551 $x2552 $x2553 $x2554 $x2555 $x2556 $x2557 $x2558 $x2559 $x2560 $x2561 $x2562 $x2563 $x2564 $x2565 $x2566 $x2567 $x2568 $x2569 $x2570 $x2571 $x2575 $x2579 $x2582 $x2587 $x2590 $x2595 $x2598 $x2604 $x2607 $x2611 $x2614 $x2620 $x2623 $x2627 $x2630 $x2636 $x2639 $x2643 $x2646 $x2652 $x2655 $x2659 $x2662 $x2668 $x2671 $x2676 $x2679 $x2684 $x2687 $x2691 $x2694 $x2700 $x2703 $x2708 $x2711 $x2717 $x2721 $x2725 $x2729 $x2733 $x2736 $x2740 $x2744 $x2748 $x2750 $x2752 $x2754 $x2756 $x2758 $x2760 $x2762 $x2764 $x2766 $x2768 $x2770 $x2772 $x2774 $x2776 $x2778 $x2780 $x2782 $x2784 $x2786 $x2788 $x2790 $x2792 $x2794 $x2796 $x2798 $x2800 $x2802 $x2804 $x2806 $x2808 $x2810 $x2812 $x2814 $x2816 $x2818 $x2819 $x2820 $x2821 $x2822 $x2823 $x2824 $x2825 $x2826 $x2827 $x2828 $x2829 $x2830 $x2831 $x2832 $x2833 $x2834 $x2835 $x2836 $x2837 $x2838 $x2843 $x2848 $x2853 $x2858 $x2861 $x2866 $x2869 $x2875 $x2878 $x2883 $x2886 $x2891 $x2894 $x2899 $x2902 $x2906 $x2909 $x2914 $x2917 $x2922 $x2926 $x2931 $x2934 $x2939 $x2941 $x2943 $x2945 $x2947 $x2949 $x2951 $x2953 $x2955 $x2957 $x2959 $x2961 $x2963 $x2969 $x2971 $x2976 $x2978 $x2983 $x2985 $x2987 $x2991 $x2996 $x3000 $x3006 $x3011 $x3014 $x3016 $x3020 $x3022 $x3023 $x3024 $x3025 $x3026 $x3030 $x3035 $x3038 $x3043 $x3046 $x3051 $x3054 $x3060 $x3063 $x3068 $x3072 $x3077 $x3081 $x3085 $x3087 $x3089 $x3091 $x3096 $x3098 $x3103 $x3105 $x3109 $x3110 $x3111 $x3112 $x3113 $x3114 $x3115 $x3116 $x3117 $x3122 $x3126 $x3132 $x3135 $x3140 $x3143 $x3148 $x3151 $x3157 $x3159 $x3161 $x3163 $x3165 $x3167 $x3173 $x3175 back_ground_feasible title_feasible main_holder_feasible less_icon_feasible github_icon_feasible dashbord_feasible search_holder_feasible mails_holder_feasible $x3177 $x3178 $x3180 $x3181 $x3183 $x3184 $x3185 $x3186 $x3188 $x3189 $x3190 $x3191 $x3193 $x3194 $x3195 $x3196 $x3197 $x3198 $x3199 $x3200 $x3202 $x3203 $x3205 $x3206 $x3208 $x3209 $x3211 $x3212 $x3214 $x3215 $x3217 $x3218 $x3220 $x3221 $x3222 $x3223 $x3224 $x3225 $x3226 $x3227 $x3228 $x3229 $x3230 $x3231 $x3232 $x3233 $x3234 $x3235 $x3236 $x3237 $x3238 $x3239 $x3240 $x3241 $x3242 $x3243 $x3244 $x3246 $x3247 $x3249 $x3250 $x3252 $x3253 $x3255 $x3256 $x3258 $x3259 $x3261 $x3262 $x3264 $x3265 $x3267 $x3268 $x3270 $x3271 $x3273 $x3274 $x3276 $x3277 $x3279 $x3280 $x3282 $x3283 $x3285 $x3286 $x3288 $x3289 $x3291 $x3292 $x3294 $x3295 $x3297 $x3298 $x3300 $x3301 $x3303 $x3304 $x3305 $x3306 $x3307 $x3308 $x3309 $x3310 $x3312 $x3313 $x3315 $x3316 $x3318 $x3319 $x3321 $x3322 $x3323 $x3324 $x3326 $x3327 $x3329 $x3330 $x3332 $x3333 $x3335 $x3336 $x3338 $x3339 $x3341 $x3342 $x3344 $x3345 $x3347 $x3348 $x3350 $x3351 $x3353 $x3354 $x3356 $x3357 $x3359 $x3360 $x3362 $x3363 $x3365 $x3366 $x3367 $x3368 $x3370 $x3371 $x3373 $x3374))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
(check-sat)

